A Connection Based Proof Method for Intuitionistic Logic

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.

• Type: Conference
• Year: 1995
• Where: TABLEAUX
• Authors: Jens Otten
• Keywords: Artificial Intelligence, Proof Method, Sequent Proof, TABLEAUX 1995, Wallen’s Matrix Characterization