Guiding Program Development Systems by a Connection Based Proof Strategy

We present an automated proof method for constructive logic based on Wallen’s matrix characterization for intuitionistic validity. The proof search strategy extends Bibel’s connection method for classical predicate logic. It generates a matrix proof which will then be transformed into a proof within a standard sequent calculus. Thus we can use an efficient proof method to guide the development of constructive proofs in interactive proof/program development systems.

• Type: Conference
• Year: 1995
• Where: LOPSTR
• Authors: Christoph Kreitz, Jens Otten, Stephan Schmitt
• Keywords: Automated Proof Method, Automated Reasoning, Efficient Proof Method, LOPSTR 1995, Proof Method