Learning Domain Knowledge to Improve Theorem Proving

               Joerg Denzinger
               Stephan Schulz

We present two learning inference control heuristics for equational
deduction. Based on data about facts that contributed to previous
proofs, evaluation functions learn to select equations that are
likely to be of use in new situations. The first evaluation function
works by symbolic retrieval of generalized patterns from a knowledge
base, the second function compiles the knowledge into abstract term
evaluation trees. We analyze the performance of the two heuristics
on a set of examples and demonstrate their usefulness. We also show
that these strategies are well suited for cooperation in the
framework of the knowledge based distribution method teamwork.