Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs
Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 190-194.
Abstract
We investigate the improvement of theorem provers by reusing previously computed proofs. A proof of a conjecture is generalized by replacing function symbols with function variables. This yields a schematic proof of a schematic conjecture which is instantiated subsequently for obtaining proofs of new, similar conjectures . Our reuse method requires solving so-called free function variables, i.e. variables which cannot be instantiated by matching the schematic conjecture with a new conjecture . We develop an algorithm for solving free function variables by combining the techniques of symbolic evaluation and second-order matching. Heuristics for controlling the algorithm are presented, and several examples demonstrate their usefulness . We also show how our reuse proposal supports the discovery of useful lemmata.
@inproceedings{ijcai1995p25,
title = {Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs},
author = {Kolbe, Thomas and Walther, Christoph},
booktitle = {Proceedings of the Fourteenth International Joint Conference on
Artificial Intelligence, {IJCAI-95}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Chris S. Mellish},
pages = {190--194},
year = {1995},
note = {Automated Reasoning},
url = {https://ijcai.org/proceedings/1995/25},
}
TY - CPAPER TI - Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs AU - Kolbe, Thomas AU - Walther, Christoph T2 - Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, IJCAI-95 PB - International Joint Conferences on Artificial Intelligence PY - 1995 SP - 190 EP - 194 UR - https://ijcai.org/proceedings/1995/25 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
