A Matrix Characterization for Multiplicative Exponential Linear Logic

Christoph Kreitz, Heiko Mantel.

Journal of Automated Reasoning 32(2):121-166, 2004.


Abstract

We develop a matrix characterization of logical validity in MELL, the multiplicative fragment of propositional linear logic with exponentials and constants. To prove the correctness and completeness of our characterization, we use a purely proof theoretical justification rather than semantical arguments.

Our characterization is based on concepts similar to matrix characterizations proposed by Wallen for other non-classical logics. It provides a foundation for developing proof search procedures for MELL by adopting techniques that are based on these concepts and also makes it possible to adopt algorithms that translate the machine-found proofs back into the usual sequent calculus for MELL.


PS Version PDF Version   (Preprint) BACK
Back to overview of papers


Bibtex Entry

@Article{ar:KreitzMantel04a, author = "Christoph Kreitz and Heiko Mantel", title = "A Matrix Characterization for {Multiplicative Exponential Linear Logic}", journal = "Journal of Automated Reasoning", year = "2004" volume = 32, number = "2", pages = "121--166", }