Converting Non-Classical Matrix Proofs into Sequent-Style Systems.
Stephan Schmitt, Christoph Kreitz.
In M. McRobbie & J. Slaney eds., 13th International Conference on Automated Deduction (CADE-13), LNCS 1104, pp. 418-432, Springer Verlag, 1996.
Abstract
	We present a uniform algorithm for transforming matrix proofs in classical, constructive, and modal logics into sequent style proofs. Making use of a similarity between matrix methods and Fitting's prefixed tableaus we first develop a procedure for extracting a prefixed sequent proof from a given matrix proof. By considering the additional restrictions on the order of rule applications we then extend this procedure into an algorithm which generates a conventional sequent proof. Our algorithm is based on unified representations of matrix characterizations for various logics as well as of prefixed and usual sequent calculi. The peculiarities of a logic are encoded by certain parameters which are summarized in tables to be consulted by the algorithm.

		Paper is available in postscript and pdf format		Slides of the conference presentation are available in compressed postscript and pdf format (Presentation: Stephan Schmitt)
Bibtex Entry					Back to overview of papers
	@InProceedings{inp:SchmittKreitz96a, author = "Stephan Schmitt and Christoph Kreitz", title = "Converting Non-Classical Matrix Proofs into Sequent-Style Systems", booktitle = "13$^{th}$ International Conference on Automated Deduction", year = 1996, editor = "M. McRobbie and J. Slaney", volume = 1104, series = "Lecture Notes in Artificial Intelligence", pages = "418--432", publisher = "Springer Verlag" }