ssssssssssssss wc E IN with each C E FP, and the C E FP with the smallest weight wc is selected.

An important property of heuristics is their fairness. A heuristic is called fair if it selects potential clauses in such a manner that no clause remains passive infinitely long. Usually the fairness of the used heuristic implies that the prover is complete, i.e. it can derive the empty clause when obtaining an inconsistent input set (provided the underlying calculus is complete).

The main strength of bottom-up calculi and provers is their strong redundancy control.

On the one hand, many inferences which are definitely unnecessary in a proof, e.g. inferences involving tautologies, are omitted. On the other hand, contraction inference rules like s ubsumption avoid the repetition of expansion inferences involving the same (or more instantiated) clauses. A big disadvantage of bottom-up calculi is their lack of goal-orientation.

Because certain inferences are favored over others due to the fixed search strategy and the heuristic weight of the clauses part of it, it might be the case that for a very long time only clauses which are not part of any proof are enumerated.

Model elimination is a typical top-down calculus which we shall introduce in the form of the connection tableau calculus ( CTC ) (Letz et al., 1994). In order to introduce CTC we want to start with the basic (free variable) tableau calculus (e.g., Fitting, 1996) for clauses.

A tableau T for C is a tree whose non-root nodes are labeled with literals and that fulfills the condition:  If the immediate successor nodes v 1 , . . , v n of a node v of T are labeled with literals l 1 , . . , l n , then the clause {l 1 , . . , l n } ( tableau clause ) is an instance of a clause in C. In the tableau calculus two inference rules are used, namely the expansion and the reduction rule (e.g., Fitting, 1996). An application of the expansion rule means selecting a clause from C and attaching the literals of a variant of it to a subgoal s which is a literal at the leaf of an open branch (a branch that does not contain two complementary literals).

Tableau reduction closes a branch by unifying a subgoal s with the complement of a literal r (denoted by ~ r) on the same branch, and applying the substitution to the whole tableau.

Connection tableau calculi work on connected tableaux. A tableau is called connected or a connection tableau if each inner node v (non-leaf node) which is labeled with literal l has a leaf node v' among its immediate successor nodes that is labeled with a literal f complementary to l. The inference rules are start, extension, and reduction. The start rule is always the first inference step of a derivation. It permits a tableau expansion that can only be applied to a trivial tableau, i.e. one consisting of only one node. Note that the start rule can be restricted to so-called start relevant clauses without causing incompleteness. Start relevancy of a clause is defined as follows. If C is an unsatisfiable set of clauses, we call S E C start relevant if there is a satisfiable subset C ′ ⊂ C such that C ′ U { S } is unsatisfiable.

Since the set of negative clauses contains at least one start relevant clause, we also consider a restricted calculus which only employs negative clauses for the start expansion (CTC neg).

The reduction rule is the same as in the conventional tableau calculus. Extension is a combination of expansion and reduction. It is performed by selecting a subgoal s in the tableau T, applying an expansion step to s, and immediately performing a reduction step with s and one of its newly created successors. Note that in the area of Horn clauses it is sufficient to employ start and extension, i.e. the reduction inference is unnecessary (e.g.,
Antoniou & Langetepe, 1994). Thus, we assume that we use versions of CTC or CTC neg that do not employ reduction steps in the area of Horn clauses.