On the Use of Subgoal Clauses in Bottom-up and Top-down Calculi

Article type: Research Article

Authors: Fuchs, Dirk

Affiliations: Fachbereich Informatik, Universität Kaiserslautern, 67663 Kaiserslautern, Germany. dfuchs@informatik.uni-kl.de

Note: [] Address for correspondence: Fachbereich Informatik, Universität Kaiserslautern, 67663 Kaiserslautern, Germany

Abstract: 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.

DOI: 10.3233/FI-1999-391207

Journal: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 123-143, 1999