ss entail a favorable rearrangement of the search because the heuristic "gets lost" in the huge nmber of clauses which can be derived from many subgoal clauses. It is hence reasonable to develop techniques for filtering subgoal clauses that appear to entail a large gain in efficiency for a superposition prover if they can be proven. That is, we are interested in filtering relevant subgoal clauses. As already described in Section 2, we generate a set of subgoal clause candidates and then we select some subgoal clauses from this set.  The chosen subgoal clauses are added to the search state of the bottom-up prover. In the following, we will at first introduce some criteria for measuring the relevancy of a clause. Then, we shall introduce two techniques for generating subgoal clause candidates and deal with the selection of relevant subgoal clauses.

## 3.2.1 Relevancy Criteria For Subgoal Clauses

Two main characteristics of subgoal clauses can contribute to a speed-up of the proof search.

Firstly, since according to Section 3.1 subgoal clauses introduce additional redundancy it is important that some of the clauses can be proven quite easily, that is more easily than the original goal(s). In order to estimate this, it is necessary to judge whether they can probably be solved with the help of clauses of the input set. Measuring similarity between a goal and other clauses with the techniques developed by Denzinger and Fuchs (1994), Denzingeret al. (1997), or Fuchs (1997) may be well-suited for this estimation.

Secondly, a solution of a newly introduced subgoal clause should not always entail a solution of an original goal within few steps of the superposition-based prover. If this were the case then the integration of new subgoal clauses would not promise much gain. Criteria in order to estimate this are: Firstly, the transformation of an original goal clause into a subgoal clause by an ME prover should have been performed by using many inferences, i.e.

k should be quite high. Then, a solution of a new subgoal clause usually does not entail a solution of an original goal within few steps because the probability is rather high that a bottom-up prover cannot —due to its heuristic search —quickly reconstruct the inferences nneeded to infer the original goal. Secondly, if there is a subgoal clause ST and some of the tableau clauses of the tableau T have a high heuristic weight w.r.t. the heuristic of the superposition-based prover, a high gain of efficiency can be expected if the prover can prove ST. This is due to the fact that inferences needed to infer the original goal using ST are difficult for the superposition-based prover.

## 3.2.2 Efficient Generation And Selection Of Subgoal Clauses

In order to generate a set of interesting subgoal clauses it is important that we employ a large resource for generating subgoal clauses. As we have already discussed, subgoal clauses that are generated with a small number of inferences do not promise much gain because a bottom-up prover may easily reconstruct the inferences needed to infer them. However, it is not possible to generate all subgoal clauses S Inf,k,c or S Inf,k,c for a sufficiently large resource k as subgoal clause candidates because their huge number means that the costs of generation and additional selection are too high. Hence, we must restrict ourselves to a set of subgoal clause candidates that is a subset of S 1 nf,k,c or S 1 nf,k,c, k sufficiently large (see Section 5).