Previous: TR 91-07 Next: TR 91-09

Intellektik: Technical report 91-08

Lemma Usage in Connection Method Theorem Proving

Gerd Neugebauer

This paper describes a method to enhance a connection method theorem prover with the ability to generate and use lemmas. This method is closely related to factorization. It can be used dynamically during a proof to avoid generating a part of the proof tree multiple times. A dual method can be obtained by studying unsolved subgoals. The combination of both features bears some complications which can be overcome by a method proposed in this paper.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry