Lemmatization is a promising way for solving "hard" problems with automated theorem provers. However, valuable results can only be reached, if the employed lemmata are restricted to useful records. The automated model-elimination theorem prover AI-SETHEO was designed for using such a controlled lemmatization from the beginning. Mainly responsible for the success of the newest version of AI-SETHEO is the implementation of an algorithm for eliminating lemma redundancies. Here, a lemma f is called redundant to other lemmata f{sub}1,…, f{sub}n, if f can be generated within very few inferences from f{sub}1,…, f{sub}n Conflicts between redundacies are resolved with an importance criterion. First experiments with AI-SETHEO give promising results.
展开▼
