A Matrix Characterization for Multiplicative Exponential Linear Logic


Christoph Kreitz, Heiko Mantel.  
Journal of Automated Reasoning 32(2):121166, 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 nonclassical 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
machinefound proofs back into the usual sequent calculus for
MELL.

(Preprint) 
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 = "121166", } 