One of the major problems in clausal theorem proving is the control of the proof search. In the presence of equality, this problem is particularly hard, since nearly all state-of-the-art systems perform the proof search by saturating a mostly unstructured set of clauses. We describe an approach that enables a superposition-based prover to pick good clauses for generating inferences based on experiences from previous successful proof searches for other problems. Information about good and bad search decisions (useful and superfluous clauses) is automatically collected from search protocols and represented in the form of annotated clause patterns. At run time, new clauses are compared with stored patterns and evaluated according to the associated information found. We describe our implementation of the system. Experimental results demonstrate that a learned heuristic significantly outperforms the conventional base strategy, especially in domains where enough training examples are available.
CITATION STYLE
Schulz, S. (2001). Learning search control knowledge for equational theorem proving. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2174, pp. 320–334). Springer Verlag. https://doi.org/10.1007/3-540-45422-5_23
Mendeley helps you to discover research relevant for your work.