Previous: TR 95-07 Next: TR 95-09

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.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry