Previous: AIDA-96-16 Next: AIDA-96-18 Index 1996

Intellectics Group: Technical Report 96-17

Connection-Based Proof Construction in Linear Logic

Christoph Kreitz and Heiko Mantel and Jens Otten and Stephan Schmitt

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 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.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry