A Matrix Characterization for MELL
by Heiko Mantel, 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
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.
bibTex ref: MK98