Options
A matrix characterization for multiplicative exponential linear logic
Publikationstyp
Journal Article
Date Issued
2004-02
Sprache
English
Author(s)
Mantel, Heiko
Journal
Volume
32
Issue
2
Start Page
121
End Page
166
Citation
Journal of Automated Reasoning 32 (2): 121-166 (2004-02)
Publisher DOI
Scopus ID
Publisher
Springer Science + Business Media B.V.
We develop a matrix characterization of logical validity in script M sign script E sign ℒ ℒ, 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 script M sign script E sign ℒ ℒ 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 script M sign script E sign ℒ ℒ.
Subjects
Automated deduction
Connection method
Linear logic
DDC Class
004: Informatik