We present a matrix characterization of logical validity in the multiplicative fragment of linear logic. On this basis we develop a matrix-based proof search procedure for this fragment and a procedure which translates the machine-found proofs back into the usual sequent calculus for linear logic. Both procedures are straightforward extensions of methods which originally were developed for a uniform treatment of classical, intuitionistic and modal logics. They can be extended to further fragments of linear logic once a matrix characterization has been found.
CITATION STYLE
Kreitz, C., Mantel, H., Otten, J., & Schmitt, S. (1997). Connection-based proof construction in linear logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1249, pp. 207–221). Springer Verlag. https://doi.org/10.1007/3-540-63104-6_20
Mendeley helps you to discover research relevant for your work.