> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/300-logic/310-mathematical-logic/tableaux.md).

# Tableaux

<https://en.wikipedia.org/wiki/Method_of_analytic_tableaux>

In proof theory, the *semantic tableau* (truth tree) is a *decision procedure* for sentential and related logics, and a *proof procedure* for formulae of FOL.

An *analytic tableau* is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula. The tableau method can also determine the *satisfiability* of finite sets of formulas of various logics.