In
proof theory, the
semantic tableau (; singular:
tableau; plural:
tableaux), also called
truth tree, is a
decision procedure for
sentential and related logics, and a
proof procedure for formulas of
first-order logic. The tableau method can also determine the
satisfiability of finite sets of
formulas of various logics. It is the most popular
proof procedure for
modal logics (Girle 2000). The method of semantic tableaux was invented by the Dutch logician
Evert Willem Beth (Beth 1955) and simplified, for classical logic, by
Raymond Smullyan (Smullyan 1968, 1995). It is Smullyan's simplification, "one-sided tableaux", that is described below. Smullyan's method has been generalized to arbitrary many-valued propositional and first-order logics by
Walter Carnielli (Carnielli 1987). Tableaux can be intuitively seen as sequent systems upside-down. This symmetrical relation between tableaux and
sequent systems was formally established in (Carnielli 1991).