Intellektik: Technical report 94-11
A Connection Based Proof Method for Intuitionistic Logic
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.
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.