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. 122137, 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 firstorder 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 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 = "122137", publisher = "Springer Verlag" } 