Improving the Performance of Automated Theorem Provers by
               Redundancy-free Lemmatization  

              Joachim Draeger and Stephan Schulz

A promising way for solving ``hard'' problems with automated theorem
provers is the lemmatization of the original problem.  The success
of this method, however, depends crucially on the selection of a
subset of lemmata that are likely to be useful.  The paper describes
an algorithm implementing the selection of lemma-knowledge by
eliminating redundant lemmata from set of potentially usable
clauses. A lemma $a$ is called redundant with respect to a lemma set
$F$, if $a$ can be generated with very few inferences from $F$.
Conflicts between redundancies are resolved with an importance
criterion. The promising results of first experiments are discussed.