Intellektik: Technical report 91-08
Lemma Usage in Connection Method Theorem Proving
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.