On the use of subgoal clauses in bottom-up and top-down calculi

• Autorzy: Fuchs D.
• Języki publikacji: EN

Abstrakty

EN

The use of lemmas is a major control tool for automated theorem proving. Many approaches for top-down or bottom-up theorem proving employ lemmas for improving the proof search. Commonly the lemmas used can be derived in a bottom-up manner using merely the given axioms. That is, top-down lemmas which represent decompositions of original proof goals did not receive much attention. We propose to systematically generate and use such goal decompositions. We introduce a notion of top-down lemmas, so-called subgoal clauses, and examine their potential to reduce proof lengths and searches in top-down and bottom-up theorem proving. Furthermore, we develop some heuristics so as to make the use of subgoal clauses efficient in practice. A case study conducted in TPTP domains with the state-of-the-art provers spass and setheo demonstrates the strength of our approach.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 1999
• Tom: Vol. 39, Nr 1,2
• Strony: 123--143
• Opis fizyczny: tab., bibliogr. 22 poz.

Twórcy

autor

Fuchs D.

• Fachbereich Informatik, Universität Kaiserslautern, 67663 Kaiserslautern, Germany,