A proof method for deductive systems appearing in the form of directed trees in which each point is a formula. Essentially, a proof by the method of tableaux is a proof by reductio ad absurdum. In the standard case of classical propositional logic, each formula of a set of assumptions $\text{Γ}$ appears at the root of the tree followed by the negation of the formula one intends to prove. One then extends these points by methodically adding individual formulae to the tree by the application of a set of rules corresponding to the consequences of the preceding formulae. For example, in the classical case of conjunction, for example, when no formula appears below a formula $\xi$ and the formula $\phi \wedge \psi$ has appeared above $\xi$ (is on the same branch as $\xi$), then because of the validity of simplification, one may add $\phi$ and $\psi$ below $\xi$, illustrated by the case:

where ‘$⋮$’ represents earlier stages in the tree. In other words, at leaf $\xi$ in a tree, if there is a path from $\phi \wedge \psi$ to that point, one may append both $\phi$ and $\psi$ and proceed with the proof.

When the truth conditions for a formula $\xi$ allow more than one circumstance under which $\xi$ may be true, the corresponding rule typically permits the addition of branches at a stage representing the possible consequences of the formulae preceding them. From a semantic perspective, in the case of a disjunction, if $\phi \vee \psi$ is true, then two possibilities exist: either $\phi$ is true or $\psi$ is true. This semantic intuition corresponds to the proof-theoretic rule that if a disjunction $\phi \vee \psi$ appears above a leaf $\xi$ in a tableau, two branches corresponding to the disjuncts may be extended from $\xi$, to which each disjunct may be added. This is represented as:

One continues the application of rules mechanically. In the classical case, if two formulae $\phi$ and $\neg \phi$ appear above a leaf $\xi$, the branch on which $\xi$ appears is called closed—usually, some mark is placed below $\xi$ to indicate this—and the application of rules to that branch ceases. In the classical case, if all branches close in a tree whose root includes each $\phi \in \text{Γ}$ and the formula $\neg \psi$, then this is construed as absurd, and one may conclude that $\psi$ is a consequence of $\text{Γ}$, i.e., that $\text{Γ}⊢\psi$ holds.

A wealth of variations on the tableau method exist, most frequently in cases in which the semantics for a deductive system is many-valued or has a semantics involving possible worlds semantics. In these cases, formulae appearing on a tree are frequently signed or labelled (whence they are frequently called labelled tableaux) by an additional syntactic marker corresponding to a semantic property. For example, in a many-valued world, points may be pairs $〈\phi ,v〉$, where $v$ stands in for a truth value or pairs $〈\phi ,w〉$ corresponding to the semantic condition that $\phi$ is true at possible world $w$. The close connection between semantics and tableau proofs often makes the construction of countermodels particularly easy, i.e., a branch that does not close frequently contains enough semantic information to give a model in which the inference $\text{Γ}⊢\phi$ fails.