(e.g., Letz et al., 1994). Therefore, a topic that has come into the focus of research is the integration of both approaches. Specifically, cooperation between theorem provers (e.g., Conry et al., 1990; Schumann, 1994; Denzinger, 1995; Bonacina & Hsiang, 1995; Bonacina, 1996; Wolf & Fuchs, 1997; Fuchs, 1998b, 1998c) based on top-down and bottom-up principles appears to be promising because by exchanging information each approach can profit from the other. It is also possible to modify calculi or provers which work according to one paradigm so as to introduce aspects of the other paradigm into it. This, however, requires a lot of implementational effort to modify the provers, whereas our approach does not require changes of the provers but only changes of their input. We can hence employ arbitrary state-of-the-art provers.

Information that is well-suited for improving the performance of top-down provers are lemmas deduced by bottom-up provers. These lemmas are added to the input of a topdown prover and can help to shorten the proof length by immediately solving subgoals.

Normally, the employed proof procedures can significantly profit from the proof length reduction obtained. The use of lemmas, however, also imports additional redundancy into the calculus. This means that an unbounded use of bottom-up generated lemmas without using techniques for choosing only relevant lemmas (i.e. lemmas which lead to a reduction of the search effort to enumerate a proof ) is not sensible. In this article, in contrast to other approaches which generate lemmas dynamically during the proof run (Astrachan & Stickel, 1992; Astrachan & Loveland, 1997), we want to employ a bottom-up prover for generating lemmas in a preprocessing phase. After the generation of a pool of lemma candidates relevant lemmas are selected from this pool and the formula to be refuted is augmented by these bottom-up generated formulas.

The second main aspect that we consider is top-down/bottom-up integration by transferring information from a top-down prover to a bottom-up prover (e.g., Fuchs, 1998a).

Our approach is to transfer top-down generated subgoal clauses - which essentially represent a transformation of an original goal clause into subgoals to a bottom-up prover and to augment its input by these clauses. This introduces a goal-oriented component into a bottom-up prover which can enable it to solve proof problems considerably faster. Hower, as is the case with lemmas, an unbounded transfer of subgoal clauses is not sensible.

Thus, we generate again subgoal clauses in a preprocessing phase and integrate only some of these clauses into the input set of a bottom-up prover. This necessitates techniques for selecting relevant subgoal clauses, i.e. techniques for selecting a set of subgoal clauses which can decrease the search effort of a bottom-up prover in order to find a proof.

In order to examine this kind of top-down/bottom-up integration we restrict ourselves to the bottom-up superposition calculus and the top-down connection tableau calculus.

These calculi are very important since they are the basis for many high-performance theorem provers. For instance, the bottom-up provers Spass (Weidenbach et al., 1996) and Gandalf (Tammet, 1997) that were most successful in recent proving competitions employ ssssee to the content of the content of the content to the content of the content to the content of the content to
(or its restriction model elimination) is also the basis for very successful top-down provers, eggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggg     1 opinion the concepts introduced for superposition and the connection tableau calculus can rather easily be transferred to other bottom-up and top-down calculi. Hence, the choice of these two calculi surely is justified.