Stephan Schulz: "Learning Search Control Knowledge for Equational
                 Theorem Proving" 

         
Abstract:

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.