Tableau method

In proof theory, the semantic tableau (/tæˈbloʊ, ˈtæbloʊ/; 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).

An analytic tableau has, for each node, a subformula of the formula at the origin. In other words, it is a tableau satisfying the subformula property.

For refutation tableaux, the objective is to show that the negation of a formula cannot be satisfied. There are rules for handling each of the usual connectives, starting with the main connective. In many cases, applying these rules causes the subtableau to divide into two. Quantifiers are instantiated. If any branch of a tableau leads to an evident contradiction, the branch closes. If all branches close, the proof is complete and the original formula is a logical truth.

...
Wikipedia