is a disjunction of conjunctions. This formula is equivalent to the set to prove unsatisfiability. The procedure modifies the tableau in such a way that the formula represented by the resulting tableau is equivalent to the original one. One of these conjunctions may contain a pair of complementary literals, in which case that conjunction is proved to be unsatisfiable. If all conjunctions are proved unsatisfiable, the original set of formulae is unsatisfiable. And Whenever a branch of a tableau contains a formula that is the conjunction of two formulae, these two formulae are both consequences of that formula. This fact can be formalized by the following rule for expansion of a tableau: () If a branch of the tableau contains a conjunctive formula , add to its leaf the chain of two nodes containing the formulae and This rule is generally written as follows: A variant of this rule allows a node to contain a set of formulae rather than a single one. In this case, the formulae in this set are considered in conjunction, so one can add at the end of a branch containing . More precisely, if a node on a branch is labeled , one can add to the branch the new leaf . Or If a branch of a tableau contains a formula that is a disjunction of two formulae, such as , the following rule can be applied: () If a node on a branch contains a disjunctive formula , then create two sibling children to the leaf of the branch, containing the formulae and , respectively. This rule splits a branch into two, differing only for the final node. Since branches are considered in disjunction to each other, the two resulting branches are equivalent to the original one, as the disjunction of their non-common nodes is precisely . The rule for disjunction is generally formally written using the symbol for separating the formulae of the two distinct nodes to be created: If nodes are assumed to contain sets of formulae, this rule is replaced by: if a node is labeled , a leaf of the branch this node is in can be appended two sibling child nodes labeled and , respectively. Not The aim of tableaux is to generate progressively simpler formulae until pairs of opposite literals are produced or no other rule can be applied. Negation can be treated by initially making