Editing Method of analytic tableaux (section)

===Connection tableau===

Connection is a condition over tableau that forbids expanding a branch using clauses that are unrelated to the literals that are already in the branch. Connection can be defined in two ways:

; strong connectedness : when expanding a branch, use an input clause only if it contains a literal that can be unified with the negation of the literal in the current leaf
; weak connectedness : allow the use of clauses that contain a literal that unifies with the negation of a literal on the branch

Both conditions apply only to branches consisting not only of the root. The second definition allows for the use of a clause containing a literal that unifies with the negation of a literal in the branch, while the first only further constraint that literal to be in leaf of the current branch.

If clause expansion is restricted by connectedness (either strong or weak), its application produces a tableau in which substitution can applied to one of the new leaves, closing its branch. In particular, this is the leaf containing the literal of the clause that unifies with the negation of a literal in the branch (or the negation of the literal in the parent, in case of strong connection).

Both conditions of connectedness lead to a complete first-order calculus: if a set of clauses is unsatisfiable, it has a closed connected (strongly or weakly) tableau. Such a closed tableau can be found by searching in the space of tableaux as explained in the "Searching for a closed tableau" section. During this search, connectedness eliminates some possible choices of expansion, thus reducing search. In other worlds, while the tableau in a node of the tree can be in general expanded in several different ways, connection may allow only few of them, thus reducing the number of resulting tableaux that need to be further expanded.

This can be seen on the following (propositional) example. The tableau made of a chain <math>true - a</math> for the set of clauses <math>\{a, \neg a \lor b, \neg c \lor d, \neg b\}</math> can be in general expanded using each of the four input clauses, but connection only allows the expansion that uses <math>\neg a \lor b</math>. This means that the tree of tableaux has four leaves in general but only one if connectedness is imposed. This means that connectedness leaves only one tableau to try to expand, instead of the four ones to consider in general. In spite of this reduction of choices, the completeness theorem implies that a closed tableau can be found if the set is unsatisfiable.

The connectedness conditions, when applied to the propositional (clausal) case, make the resulting calculus non-confluent. As an example, <math>\{a, b, \neg b\}</math> is unsatisfiable, but applying <math>(C)</math> to <math>a</math> generates the chain <math>true - a</math>, which is not closed and to which no other expansion rule can be applied without violating either strong or weak connectedness. In the case of weak connectedness, confluence holds provided that the clause used for expanding the root is relevant to unsatisfiability, that is, it is contained in a minimally unsatisfiable subset of the set of clauses. Unfortunately, the problem of checking whether a clause meets this condition is itself a hard problem. In spite of non-confluence, a closed tableau can be found using search, as presented in the "Searching for a closed tableau" section above. While search is made necessary, connectedness reduces the possible choices of expansion, thus making search more efficient.