Learning Search Control Knowledge for Equational Deduction

                  Stephan Schulz

Automated theorem provers for first order logic are increasingly being
used in formal mathematics or for verification tasks. For these
applications, efficient treatment of the equality relation is
particularly important. Due to the special properties of the equality
relation, the proof search is particularly hard for problems
containing equality, even if state of the art calculi are used.

In this thesis we develop techniques to automatically learn good
search heuristics to control the proof search of a superposition-based
theorem prover for clausal logic with equality. We describe a variant
of the superposition calculus and an efficient proof procedure
implementing this calculus. An analysis of the choice points of this
algorithm shows that the order in which new logical consequences are
being processed by the prover is the single most important decision
during the proof search.

We develop methods to extract information about important good and bad
search decisions from existing proof searches. These search decisions
are represented by signature-independed annotated epresentative
  clause patterns, which represent all analogous search decision by a
single unique term. Annotations carry information about the role of
the seach decisions in different proof attempts.

To utilize the stored knowledge for a new proof attempt, experiences
generated from proof problems similar to the one at hand are extracted
from the stored knowledge. The selected proof experiences, represented
by a set of patterns with associated evaluations, are used as input
for a new, hybrid learning algorithm which generates a term
  space map, a structure that allows the evaluation of new potential
search decisions.

We experimentally demonstrate the performance of different variants of
the term space mapping algorithm for artificial term classification
problems as well as a siginificant gain in performance for the
learning theorem prover E/TSM compared to the variant using only
conventional search heuristics.