On Transforming Intuitionistic Matrix Proofs into Standard-Sequent 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. 106-121, 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 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.


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
Back to overview of papers
@InProceedings{inp:SchmittKreitz95a, author = "Stephan Schmitt and Christoph Kreitz", title = "On Transforming Intuitionistic Matrix Proofs into Standard-Sequent 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 = "106--121", publisher = "Springer Verlag" }