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

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