CTC or CTC neg do not have specific inference rules for handling equality. Instead, when dealing with equality, the axiomatization must be extended by the reflexivity, symmetry, transitivity, and substitution axioms of the equality symbol. Indeed, the use of an axiomatic form of equality is in no sense optimal. But it is very difficult to develop methods for using built-in equality in tableau calculi that yield convincing results in practice.

If a subgoal s becomes (after some inferences) head of a closed (sub-)tableau we call the obt ained substitution a solution of s.

The notion of a tableau derivation and a search tree is important: We say T H T if (and only if) tableau T ′ can be derived from T by applying a start rule if T is the trivial tableau, or by an extension/reduction rule to a subgoal in T . The connection tableau calculus is not
(proof) confluent. In order to show the unsatisfiability of a clause set C, a search tree, given as follows, has to be examined in a fair way (each node of the tree must be visited after a finite amount of time) until a closed tableau occurs. A search tree T defined by a calculus and a set of clauses C is given by a tree whose root is labeled with the trivial tableau. Every inner node in T labeled with tableau T has as immediate successors the nodes from the maximal set { v 1 , . . , v n }, where v i is labeled with T i and T H T i , 1 < i < n.

Since not only the number of proof objects but also their size increases during the proof process, explicit tableaux enumeration procedures that construct all tableaux in T in a breadth-first manner are not reasonable. Hence, implicit enumeration procedures that apply consecutively bounded iterative deepening search with backtracking (Korf, 1985) are normally used. In this approach iteratively larger finite initial parts of the search tree T are explored with depth-first search. A finite segment is normally defined by a so-called completeness bound (which poses structural restrictions on the tableaux which are allowed in the current ssegment, see below) and a fixed natural number, a so-called resource. Iterative deepening is performed by starting with a basic resource value n E IN and iteratively increasing n until a proof is found within the finite initial segment of T defined by one bound and n. Prominent examples for completeness bounds are the depth bound, inference bound, and weighted-depth bound The depth bound limits the maximal depth of inner nodes (non-leaf nodes) in a tableau where the current resource n is the maximal depth permitted (the root node has depth 0).

In practice, the depth bound is quite successful (Letz et al., 1994; Harrison, 1996) but it suffers from the large increase of the segment (defined by a resource n ) caused by an increase of n. The inference bound allows a level by level exploration of the search tree (e.g., Stickel, 1988). In companson with the depth bound, the inference bound makes a smooth increase of the search space possible, but it is infenor to the depth bound in practice. In order to combine the advantages of the depth and the inference bound, the weighted-depth bound was introduced by Moseret al. (1997). This bound describes a class of possible bounds that restrict the tableau depth and the number of inferences allowed to infer a specific tableau.

Goal-orientation of CTC', as our typical top-down calculus, is given by the connected ness condition. This condition entails that every literal in a tableau bears a relation to the start clause. The set of possible start clauses can normally be restricted to quite a small set of clauses which are sufficient in order to guarantee completeness (e.g., Moser et al., 1997),
eg, the set of negative clauses as already mentioned. Thus, only certain descendants having a connection to a start (goal) clause are enumerated. A main problem of proofs with CTC