On Transforming Intuitionistic Matrix Proofs into StandardSequent Proofs.


Stephan Schmitt, Christoph Kreitz.  
In P. Baumgartner, R. Hähnle, J. Posegga, eds., 4th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX'95), LNCS 918, pp. 106121, Springer Verlag, 1995. 

Abstract 

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
nonstandard sequent calculus our procedure consists of two
steps. First a nonstandard sequent proof will be extracted from a
given matrix proof. Secondly we transform each nonstandard 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.

Paper is available in
postscript and pdf format 
Slides of the conference presentation are available
in compressed postscript and
pdf format
(Presentation: Stephan Schmitt) 

Bibtex Entry 
Back to overview of papers 

@InProceedings{inp:SchmittKreitz95a, author = "Stephan Schmitt and Christoph Kreitz", title = "On Transforming Intuitionistic Matrix Proofs into StandardSequent Proofs", booktitle = "4$^t{}^h$ Workshop on Theorem Proving with Analytic Tableaux and Related Methods", year = 1995, editor = "P. Baumgartner and R. H{\"a}hnle and J. Posegga", volume = 918, series = "Lecture Notes in Artificial Intelligence", pages = "106121", publisher = "Springer Verlag" } 