---
title: "Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs"
authors:
  - "Thomas Kolbe"
  - "Christoph Walther"
doi: ""
url: "https://ijcai.org/proceedings/1995/25"
pdf: "https://ijcai.org/proceedings/1995/0025.pdf"
venue: "Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence"
year: 1995
pages: "190-194"
track: "Automated Reasoning"
keywords:
---

# Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs

Thomas Kolbe, Christoph Walther

*Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence*, 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.