Intellektik: Technical report 95-08
Guiding Program Development Systems by a Connection Based Proof Strategy
Christoph Kreitz, Jens Otten and Stephan Schmitt
We present an automated proof method for constructive logic ba
sed 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.