Previous: TR 94-09 Next: TR 94-11


Intellektik: Technical report 94-10

On Transforming Intuitionistic Matrix Proofs into Standard-Sequent Proofs

Stephan Schmitt and Christoph Kreitz


We present a procedure transforming intuitionistic matrix proofs into proofs within the intuitionistic standard sequent calculus. The transformation is based on L.~Wallen's proof justifying his matrix characterization for the validity of intuitionistic formulae. Since this proof makes use of Fitting`s non-standard sequent calculus our procedure consists of two steps. First a non-standard sequent proof will be extracted from a given matrix proof. Secondly we transform each non-standard proof into a standard proof in a structure preserving way. To simplify the latter step we introduce an extended standard calculus which is shown to be sound and complete.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry