A Matrix Characterization for MELL
Heiko Mantel, Christoph Kreitz · TUbilio (Technical University of Darmstadt) · 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 matrixbased proof search procedures for MELL as well as for procedures which translate machine-found proofs back into the usual sequent calculus. 1 Introduction Linear logic [12] has become known as a very expressive formalism for reasoning about action and change. During its rather rapid development linear logic has found applications in logic programming [14,19], modeling concurrent computation [11], planning [18], and other areas. Its expressiveness, however, results in a high complexity. Propositional linear logic is undecidable. The multiplicative fragment (MLL) is already NP-complete [16]. The complexity of the multiplicative exponential fragment (MELL) is still unknown. Consequently, proof search in linear log...