A Matrix Characterization of MELL

unofficial copies [PDF], [PS]

by Heiko Mantel and Christoph Kreitz

Proceedings of Sixth European Workshop on Logics in Artificial Intelligence (JELIA'98), J. Dix, F. L. Del Cerro, and U. Furbach (eds.), LNAI 1489, pp. 169-183, Springer-Verlag, 1998.


We present a matrix characterization of logical validity in the multiplicative fragment of linear logic with exponentials. In the process we elaborate a methodology for proving matrix characterizations correct and complete. Our characterization provides a foundation for a matrix-based proof search procedure for MELL as well as for a procedure which translates the machine-found proofs back into the usual sequent calculus.

Slides of the conference presentation are available in compressed PS and PDF format. (Presentation: Heiko Mantel)