Adaptation of Proofs for Reuse

Thomas Kolbe & Christoph Walther

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.