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

Joachim Draeger and Stephan Schulz, Technische Universität München, Germany

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


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.