A Connection Based Proof Method for Intuitionistic Logic.

Jens Otten, 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. 122-137, Springer Verlag, 1995.


Abstract

We present a proof method for intuitionistic logic based on Wallen's matrix characterization. Our approach combines the connection calculus and the sequent calculus. The search technique is based on notions of paths and connections and thus avoids redundancies in the search space. During the proof search the computed first-order and intuitionistic substitutions are used to simultaneously construct a sequent proof which is more human oriented than the matrix proof. This allows to use our method within interactive proof environments. Furthermore we can consider local substitutions instead of global ones and treat substitutions occurring in different branches of the sequent proof independently. This reduces the number of extra copies of formulae to be considered.


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




Bibtex Entry


BACK
Back to overview of papers
@InProceedings{inp:OttenKreitz95a, author = "Jens Otten and Christoph Kreitz", title = "A Connection Based Proof Method for Intuitionistic Logic", 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 = "122--137", publisher = "Springer Verlag" }