Previous: AIDA-95-14 Next: AIDA-96-02 Index 1996

Intellectics Group: Technical report 96-01

On Converting Non-classical Matrix Proofs into Sequent-Style Systems

Christoph Kreitz and Stephan Schmitt

We present a uniform algorithm for transforming matrix proofs in classical, constructive, and modal logics into sequent style proofs. It can serve as the key step in a conversion of automatically generated proofs into a humanly comprehensible form and will be presented in two phases. Making use of a similarity between matrix characterizations of logical validity and Fitting's prefixed tableaux systems we first develop a method for extracting a prefixed sequent proof from a given matrix proof. By considering additional wait-labels which restrict the order of rule applications we then extend this method into an algorithm which converts a matrix proof into a proof within a usual sequent calculus.

Our procedure is based on unified representations of matrix characterizations of logical validity with respect to various logics as well as of prefixed and conventional sequent calculi for these logics. The peculiarities of a logic are encoded by certain parameters of these representations and summarized in tables which will be consulted by our transformation algorithm. This allows us to treat different logics in a uniform way.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry