may occur in more than one branch (this is the case if there is at least a branching point "below" the node). In this case, the rule for expanding the formula has to be applied so that its conclusion(s) are appended to all of these branches that are still open, before one can conclude that the tableau cannot be further expanded and that the formula is therefore satisfiable. Set-labeled tableau A variant of tableau is to label nodes with sets of formulae rather than single formulae. In this case, the initial tableau is a single node labeled with the set to be proved satisfiable. The formulae in a set are therefore considered to be in conjunction. The rules of expansion of the tableau can now work on the leaves of the tableau, ignoring all internal nodes. For conjunction, the rule is based on the equivalence of a set containing a conjunction with the set containing both and in place of it. In particular, if a leaf is labeled with , a node can be appended to it with label : For disjunction, a set is equivalent to the disjunction of the two sets and . As a result, if the first set labels a leaf, two children can be appended to it, labeled with the latter two formulae. Finally, if a set contains both a literal and its negation, this branch can be closed: A tableau for a given finite set X is a finite (upside down) tree with root X in which all child nodes are obtained by applying the tableau rules to their parents. A branch in such a tableau is closed if its leaf node contains "closed". A tableau is closed if all its branches are closed. A tableau is open if at least one branch is not closed. Here are two closed tableaux for the set X = {r0 & ~r0, p0 & ((~p0 ∨ q0) & ~q0)} with each rule application marked at the right hand side (& and ~ stand for and , respectively) {r0 & ~r0, p0 & ((~p0 v q0) & ~q0)} {r0 & ~r0, p0 & ((~p0 v q0) & ~q0)} --------------------------------------(&) ------------------------------------------------------------(&) {r0, ~r0, p0 & ((~p0 v q0) & ~q0)} {r0 & ~r0, p0, ((~p0 v q0) & ~q0)} -------------------------------------(id) ----------------------------------------------------------(&) closed {r0 & ~r0, p0, (~p0 v q0), ~q0} -------------------------------------------------------------(v) {r0 & ~r0, p0, ~p0, ~q0} | {r0