A Matrix Characterization for MELL

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 matrixbased proof search procedures for MELL as well as for procedures which translate machine-found proofs back into the usual sequent calculus.

• Type: Conference
• Year: 1998
• Where: JELIA
• Authors: Heiko Mantel, Christoph Kreitz
• Keywords: Artificial Intelligence, JELIA 1998, Matrix Characterizations, Proof Search Procedures, Usual Sequent Calculus