

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

is that in general they are rather long. In fact, CTC is among the weakest calculi when the lengths of existing proofs are considered. Therefore, Letz et al. (1994) proposed extensions of CTC which are based on a controlled integration of the cut rule. These extensions can also be seen as restricted lemma mechanisms. A further problem is that often during the sseeeeeerrrreeeerrreeerrreeerreeerreeerreeerreeerreeerreeerreeerreeerreeerreee extensions of the calculus proposed to overcome such problems. E.g., by Letz et al. (1994)
a restricted subsumption concept and by Astrachan and Stickel (1992) caching techniques have been introduced.

## 2.2 Achieving Cooperation By Preprocessing And Input Augmentation

Our approach of integrating top-lown and bottom-up provers by cooperation is characterized by preprocessing and inpul augmentation. Henceforth, let C be the initial clause set whose inconsistency should be shown. In the preprocessing phase the bottom-up superposition prover generates a set of clauses CBU such that C |= CBU. Analogously, we extract from a certain number of proof attempts of the ME prover a clause set CTD such that C |= CTD. Then, the input set C of the superposition prover is augmented by CTD.

and the input of the ME prover with CBU. After that both provers can proceed to work in parallel. Figure 1 displays this kind of cooperation that is essentially based on a sequential concatenation of both provers. The approach can be seen as a specific instantiation of the general cooperation approach TECHS (Denzinger & Fuchs, 1998).

Since the superposition prover works on a search state which contains a set of clauses, it is very easy to generate a set of valid clauses in a preprocessing phase. A very simple method is to perform a fixed number i of activation steps and to generate the clause sets FA,i and FP,i of active and passive clauses. Then, we select all facts, i.e. positive unit clauses, from FA,, Since the inferences of a superposition-based prover are sound, it produces only logic consequences of C. As we shall explain in Section 4 in more detail, it is not sensible to add all generated positive units to the input of the top-down prover, i.e. to set CBU = {C : C is a fact, C E FAi}. However, it is wise to select only some units with a function ϕ BU , i.e. C BU = ϕ BU ({C': C is a fact, C E F A,i}).

Because connection tableau-based provers have asearch state which contains deductions
(tableaux) instead of clauses, it is at first sight not obvious how to extract valid clauses from such a search state which will be well-suited for a superposition-based prover. A