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.