Termination of theorem proving by reuse

Abstract

We investigate the improvement of theorem provers by reusing previously computed proofs. We formulate our method for reusing proofs as an instance of the problem reduction paradigm and then develop a termination requirement for our reuse procedure. We prove the soundness of our proposal and show that reusability of proofs is not spoiled by the termination requirement imposed on the reuse procedure. We also give evidence for the general usefulness of our termination requirement for lemma speculation in induction theorem proving.