# 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.