Previous: TR 94-10 Next: TR 94-12

Intellektik: Technical report 94-11

A Connection Based Proof Method for Intuitionistic Logic

C. Kreitz

We present a proof method for intuitionistic logic based on Wallen's matrix characterization. Our approach is a combination of the connection calculus and the sequent calculus. The search technique is based on notions of paths and connections as in Bibel's connection calculus. During the proof search the corresponding sequent proof is constructed using the computed first-order and so-called intuitionistic substitutions. Whereas the connection-based technique is directed towards avoiding redundancies in the search space the sequent proof derived simultaneously is more human oriented. Our method can therefore be used within interactive proof environments. The sequent proof also makes it possible to use local substitutions instead of global ones. Thus the substitutions of different branches in the sequent proof can be treated independently. This reduces the number of extra copies of formulae to be considered during the proof process.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry