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.