On the Use of Subgoal Clauses in Bottom-up and Top-down Calculi
Dirk Fuchs · Fundamenta Informaticae · 1999
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 merel