Learning Search Control Knowledge for Equational Deduction, Vol. 230 Book

Techniques for handling of the equality relation are essential for the successful application of theorem provers to most interesting first order problems. The currently best approach to this field is the superposition calculus. This saturating calculus systematically generates logical consequences from a set of axioms and thus tries to find a proof for the hypothesis. The most important decision for the success of the proof search is the order in which potential new consequences are considered. This thesis presents an approach to learn good search guiding heuristics for the superposition-based theorem prover E. Search decisions from successful proof searches are represented as sets annotated clause patterns. Term Space Mapping, a new learning method for recursive structures, is used to learn heuristic evaluation functions for the evaluation of potential new consequences. Experimental results with the extended system E/TSM show the success of the approach. Additional contributions of the thesis are an extended superposition calculus and a description of both the proof procedure and the implementation of a state-of-the-art equational theorem prover.