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

May 2001

Proceedings of the Fourteenth International Florida Artificial Intelligence Research Society Conference (FLAIRS 2001)

Volume

Proceedings of the Fourteenth International Florida Artificial Intelligence Research Society Conference (FLAIRS 2001)

All Papers

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