A Matrix Characterization for Multiplicative Exponential Linear Logic

摘要

We develop a matrix characterization of logical validity in M&LL, the multiplicative fragment of prepositional 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 M&LL 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 M&LL.