Method of analytic tableaux

In proof theory, the semantic tableau[1] (/tæˈbloʊ, ˈtæbloʊ/; plural: tableaux), also called an analytic tableau,[2] truth tree,[1] or simply tree,[2] is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic.

The main principle of propositional tableaux is to attempt to "break" complex formulae into smaller ones until complementary pairs of literals are produced or no further expansion is possible.

At each step, this tree is modified; in the propositional case, the only allowed changes are additions of a node as descendant of a leaf.

The procedure starts by generating the tree made of a chain of all formulae in the set to prove unsatisfiability.

The aim of tableaux is to generate progressively simpler formulae until pairs of opposite literals are produced or no other rule can be applied.

[14] Tableaux are extended to first-order predicate logic by two rules for dealing with universal and existential quantifiers, respectively.

A solution to this problem is to "delay" the choice of the term to the time when the consequent of the rule allows closing at least a branch of the tableau.

What is gained by this change is that these variables can be then given a value when a branch of the tableau can be closed, solving the problem of generating terms that might be useless.

The formula represented by a tableau is obtained in a way that is similar to the propositional case, with the additional assumption that free variables are considered universally quantified.

For first-order tableaux without unification, the condition of fairness is similar, with the exception that the rule for universal quantifiers might require more than one application.

As a result, completeness does not automatically imply the existence of a feasible policy of application of rules that always leads to a closed tableau for every given unsatisfiable set of formulae.

A general solution for this problem is that of searching the space of tableaux until a closed one is found (if any exists, that is, the set is unsatisfiable).

Different methods for reducing search disallow the generation of some tableaux on the ground that a closed tableau can still be found by expanding the other ones.

This restriction reduces the search space because one possible choice is now forbidden; completeness is however not harmed, as the second branch will still be expanded if the first one is eventually closed.

When applied to sets of clauses (rather than of arbitrary formulae), tableaux methods allow for a number of efficiency improvements.

That free variables are universally quantified is not a consequence of the definition of first-order satisfiability; it is rather used as an implicit common assumption when dealing with clauses.

When the set to be checked for satisfiability is only composed of clauses, this and the unification rules are sufficient to prove unsatisfiability.

If clause expansion is restricted by connectedness (either strong or weak), its application produces a tableau in which substitution can applied to one of the new leaves, closing its branch.

Both conditions of connectedness lead to a complete first-order calculus: if a set of clauses is unsatisfiable, it has a closed connected (strongly or weakly) tableau.

In spite of this reduction of choices, the completeness theorem implies that a closed tableau can be found if the set is unsatisfiable.

The connectedness conditions, when applied to the propositional (clausal) case, make the resulting calculus non-confluent.

Modal tableaux calculi do contain rules of the kind of the one above, but include mechanisms to avoid the incorrect interaction of formulae referring to different worlds.

Tableaux calculi for modal logic take into account that formulae may refer to different worlds.

As a result, the relative (modal) tableau expansion rule is static, as both its precondition and consequence refer to the same world.

This condition is initially true as all formulae in the set to be checked for consistency are assumed referring to the same world.

All propositional expansion rules are adapted to this variant by stating that they all refer to formulae with the same world label.

This condition is automatically captured by set-labeling tableaux, as expansion rules are based only on the leaf where they are applied and not on its ancestors.

Having a large number of possible choices makes the problem of searching for a closed tableau harder.

The above modal tableaux establish the consistency of a set of formulae, and can be used for solving the local logical consequence problem.

Tableaux calculi can deal with global assumption by a rule allowing its addition to every node, regardless of the world it refers to.