and automated reasoning. Note that this larger tree is present regardless of whether the nodes contain sets, multisets, lists or trees. Propositional logic This section presents the tableau calculus for classical propositional logic. A tableau checks whether a given set of formulae is satisfiable or not. It can be used to check either validity or entailment: a formula is valid if its negation is unsatisfiable and formulae imply if is unsatisfiable. The main principle of propositional tableaux is to attempt to "break" complex formulae into smaller ones until complementary pairs of literals are produced or no further expansion is possible. The method works on a tree whose nodes are labeled with formulae. At each step, this tree is modified; in the propositional case, the only allowed changes are additions of a node as descendant of a leaf. The procedure starts by generating the tree made of a chain of all formulae in the set to prove unsatisfiability. (A variant to this starting step is to begin with a single-node tree whose root is labeled by ; in this second case, the procedure can always copy a formula in the set below a leaf. As a running example, the tableau for the set is shown.) Then, the following procedure may be repeatedly applied nondeterministically: Pick an open leaf node. (The leaf node in the initial chain is marked open). Pick an applicable node on the branch above the selected node. Apply the applicable node, which corresponds to expanding the tree below the selected leaf node based on some expansion rule (detailed below). For every newly-created node that is both a literal/negated literal, and whose complement appears in a prior node on the same branch, mark the branch as closed. Mark all other newly-created nodes as open. (An applicable node is a node whose outermost connective corresponds to an expansion rule, and which has not already been applied at any prior node on the selected leaf node's branch.) Eventually, this procedure will terminate, because at some point every applicable node gets applied, and the expansion rules guarantee that every node in the tree is simpler than the applicable node used to create it. The principle of tableau is that formulae in nodes of the same branch are considered in conjunction while the different branches are considered to be disjuncted. As a result, a tableau is a tree-like representation of a formula that