Tableau Glossary
Definition
A semantic tableau is a structure encoding a semantic analysis of a set of formulae. It consists of a tree, each node of which is essentially a set of formulae each labelled as true or false. The successors of a node result from it by spelling out the requirements for one of the formulae to have the truth value given in its label.
A tableau branch is closed if it contains a contradiction—i.e. a formula labelled with two different truth values—and open otherwise. A completed open branch shows the existence of an interpretation satisfying the assignments at the root of the tableau; a tableau in which all branches are closed shows unsatisfiability and can be read as a proof.
Comments
Tableaux can be written in several ways. The entire set of formulae can be written out at each node, or just the formula being analysed may be written. Truth value labels may be written explicitly (as is done in these notes) or the true label may be omitted and the false one emulated by writing the negation of the formula, resulting in "unlabelled tableaux". The tableau may be drawn branching downwards, with its root at the top, or upwards with its root at the bottom. Clearly, none of this makes any real difference.
For classical propositional logic, the tableau method constitutes a decision procedure—i.e. a completely mechanical method guaranteed to determine whether a formula is satisfiable or not. By starting with the assumptions that all premises are true and the conclusion false, we can thus decide whether a given finite sequent is valid or not. For first order logic, this is not the case, though we can be sure that the sequent is valid if and only if there is a closed tableau for it.
Examples
See the links below for examples of tableaux.