

![0_image_0.png](0_image_0.png)

Our first variant, an inference-based method, starts by generating subgoal clauses from S Inf ,k,C or S Inf ,k,C for a rather large resource k and stops when N sg subgoal clause candidates are generated. The advantage of this method is that it is very easy and can be efficiently implemented. Tableaux are enumerated with a fixed strategy for selecting subgoals for inferences (usually left-most/depth-first) and for each tableau its subgoal clause is stored.

The main disadvantage of this method is that due to the fixed strategy and the limit of the number of subgoal clauses, we only obtain subgoal clauses which are inferred from goal clauses by expanding particular subgoals with a large number of inferences and other subgoals with only a small number of inferences. (See also Figure 2: Ovals are tableaux in a finite segment of the search tree T, the lines represent the H relation.  Grey ovals represent enumerated tableaux, i.e. their subgoal clauses are stored, white ovals represent tableaux which are not enumerated.) Thus, the method is somewhat unintelligent because no information about the quality of the transformation of an original goal clause into a subgoal clause is used. Certain transformations are favored against others only due to the uninformed subgoal selection strategy.

Our second vanant, an adaptive method, tries to overcome these disadvantages in the following way: Instead of permitting more inferences when generating subgoal clauses due to an uninformed subgoal selection strategy, we want to allow more inferences at certain interesting positions of the search tree T for a given set of clauses C.

In detail, our approach is as follows: At first, we generate all subgoal clauses S Inf,k 1,C
or S I n f,k 1,C with a resource k 1 which is smaller compared to the first variant. Then, a fixed number N n f of subgoal clauses is chosen which promise the highest gain of efficiency regarding the previously mentioned criteria. More exactly, we choose subgoal clauses which are maximal w.r.t. a selection function ψ. One possible realization of ψ is:

$\psi(S_{T})=\alpha_{1}\cdot I(S_{T})+\alpha_{2}\cdot\max\left(\left\{\mathcal{H}\left(C\right):C\text{is a tableau clause in}T\right\}\right):$  $$+\alpha_{3}\cdot\max\left(\left\{\,\dot{s}\,im(S_{T},C\,):C\in\mathcal{C},\left|C\right|=1\,\right\}\right)$$
The higher the number of inferences I(ST) which are needed to infer ST, the higher
$(ST) should be. Hence, a1 should be positive. Setting a2 > 0 is also sensible. If there