Abstract:

A Matrix Characterization for Multiplicative Exponential Linear Logic

Christoph Kreitz and Heiko Mantel


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.