Adaptation of Proofs for Reuse

Contents

Automated theorem provers might be improved if they are enabled to reuse previously computed proofs. Our approach for reuse is based on generalizing computed proofs by replacing function symbols with function variables. This yields a schematic proof which is instantiated subsequently for obtaining proofs of new, similar conjectures. Our reuse method requires two steps of proof adaptation, viz. the solution of so-called free function variables and the patching of completely instantiated proofs. We develop algorithms for solving free function variables and for computing patched proofs and demonstrate their usefulness with several examples.