Improving the Performance of Automated Theorem Provers by Redundancy-Free Lemmatization
Joachim Draeger, Stephan Schulz · 2001
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. Keywords: theorem proving, lemmatization, redundancy elimination