Converting NonClassical Matrix Proofs into SequentStyle Systems.


Stephan Schmitt, Christoph Kreitz.  
In M. McRobbie & J. Slaney eds., 13th International Conference on Automated Deduction (CADE13), LNCS 1104, pp. 418432, 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 NonClassical Matrix Proofs into SequentStyle 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 = "418432", publisher = "Springer Verlag" } 