Connection-Based Proof Construction in Linear Logic.
Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt.
In W. McCune, ed., 14th International Conference on Automated Deduction (CADE-14), LNAI 1249, pp. 207-221, Springer Verlag, 1997.
Abstract
	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.

		Paper is available in postscript and pdf format		Slides of the conference presentation are available in compressed postscript and pdf format (Presentation: Heiko Mantel)
Bibtex Entry					Back to overview of papers
	@InProceedings{inp:KreitzMantelOttenSchmitt97a, author = "Christoph Kreitz and Heiko Mantel and Jens Otten and Stephan Schmitt", title = "Connection-Based Proof Construction in Linear Logic", booktitle = "14$^{th}$ International Conference on Automated Deduction", year = 1997, editor = "W. McCune", volume = 1249, series = "Lecture Notes in Artificial Intelligence", pages = "207--221", publisher = "Springer Verlag" }