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.