Tableau method and its importance

The tableau method (semantic tableau or truth tree) is a systematic refutation procedure for propositional logic. To test a formula, we write it at the root of a tree and break it into simpler formulas using fixed rules until only literals (variables or negated variables) remain.

Definition and rules

• α-rules (conjunction type, no branching): A∧B gives A, B on the same branch; ¬(A∨B) gives ¬A, ¬B; ¬(A→B) gives A, ¬B.
• β-rules (disjunction type, branching): A∨B gives A | B; A→B gives ¬A | B; ¬(A∧B) gives ¬A | ¬B.
• ¬¬A is replaced by A.
• A branch is closed (marked ×) if it contains a complementary pair, say p and ¬p. It is open if it is fully expanded and has no such pair.
• If every branch is closed, the tableau is closed; otherwise it is open.

Why it is important

1. Decision procedure. For a propositional formula the tableau always terminates, so it decides satisfiability mechanically.
2. Tests validity. A formula A is valid (a tautology) if and only if the tableau of ¬A is closed. It is unsatisfiable if its own tableau is closed.
3. Gives models and counterexamples. Each open branch directly gives an assignment that makes the formula true (or, for ¬A, a counterexample to A).
4. Checks arguments. Premises A₁,…,Aₙ imply a conclusion C if the tableau of {A₁,…,Aₙ, ¬C} is closed.
5. Efficient. It avoids writing a full truth table of 2ⁿ rows, because a branch is dropped as soon as it closes.
6. Foundation of automated reasoning. It is sound and complete, and it extends to predicate logic and is used in theorem provers.