In proof theory, the semantic tableau[1] (; plural: tableaux), also called an analytic tableau,[2] truth tree, or simply tree, is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic. 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. It is the most popular proof procedure for modal logics.
A method of truth trees contains a fixed set of rules for producing trees from a given logical formula, or set of logical formulas. Those trees will have more formulas at each branch, and in some cases, a branch can come to contain both a formula and its negation, which is to say, a contradiction. In that case, the branch is said to close. If every branch in a tree closes, the tree itself is said to close. In virtue of the rules for construction of tableaux, a closed tree is a proof that the original formula, or set of formulas, used to construct it was itself self-contradictory, and therefore false. Conversely, a tableau can also prove that a logical formula is tautologous: if a formula is tautologous, its negation is a contradiction, so a tableau built from its negation will close.
In his Symbolic Logic Part II, Charles Lutwidge Dodgson (also known by his literary pseudonym, Lewis Carroll) introduced the Method of Trees, the earliest modern use of a truth tree.
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). Smullyan's simplification, "one-sided tableaux", is described here. 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).
A formula in propositional logic consists of letters, which stand for propositions, and connectives for conjunction, disjunction, conditionals, biconditionals, and negation. The truth or falsehood of a proposition is called its truth value. A formula, or set of formulas, is said to be satisfiable if there is a possible assignment of truth-values to the propositional letters such that the entire formula, which combines the letters with connectives, is itself true as well. Such an assignment is said to satisfy the formula.
A tableau checks whether a given set of formulae is satisfiable or not. It can be used to check either validity or entailment: a formula is valid if its negation is unsatisfiable, and formulae
A1,\ldots,An
B
\{A1,\ldots,An,\negB\}
The following table shows some notational variants for logical connectives, for readers who may be more familiar with a different notation from the one used here. In general, as of the time of the inclusion of this sentence, the first symbol in each line has been used in the text of this article; however, since Wikipedia editors are not rule-bound to use consistent notation within or between articles, this may change.
| Connective | Symbol | |
|---|---|---|
| AND | A\landB A ⋅ B AB A\&B A\&\&B | |
| equivalent | A\equivB A\LeftrightarrowB A\leftrightharpoonsB | |
| implies | A ⇒ B A\supsetB A → B | |
| NAND | A\overline{\land}B A\midB \overline{A ⋅ B} | |
| nonequivalent | A\not\equivB A\not\LeftrightarrowB A\nleftrightarrowB | |
| NOR | A\overline{\lor}B A\downarrowB \overline{A+B} | |
| NOT | \negA -A \overline{A} \simA | |
| OR | A\lorB A+B A\midB A\parallelB | |
| XNOR | A B | |
| XOR | A\underline{\lor}B A ⊕ B |
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.
The method works on a tree whose nodes are labeled with formulae. 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.[5] Then, the following procedure may be repeatedly applied nondeterministically:
Eventually, this procedure will terminate, because at some point every applicable node gets applied, and the expansion rules guarantee that every node in the tree is simpler than the applicable node used to create it.
The principle of tableau is that formulae in nodes of the same branch are considered in conjunction while the different branches are considered to be disjuncted. As a result, a tableau is a tree-like representation of a formula that is a disjunction of conjunctions. This formula is equivalent to the set to prove unsatisfiability. The procedure modifies the tableau in such a way that the formula represented by the resulting tableau is equivalent to the original one. One of these conjunctions may contain a pair of complementary literals, in which case that conjunction is proved to be unsatisfiable. If all conjunctions are proved unsatisfiable, the original set of formulae is unsatisfiable.
Whenever a branch of a tableau contains a formula
A\wedgeB
() If a branch of the tableau contains a conjunctive formula\wedge
, add to its leaf the chain of two nodes containing the formulaeA\wedgeB
andA
B
This rule is generally written as follows:
(\land)
| A\wedgeB | |
| \begin{array |
{c}A\ B\end{array}}
A variant of this rule allows a node to contain a set of formulae rather than a single one. In this case, the formulae in this set are considered in conjunction, so one can add
\{A,B\}
A\wedgeB
X\cup\{A\wedgeB\}
X\cup\{A,B\}
If a branch of a tableau contains a formula that is a disjunction of two formulae, such as
A\veeB
() If a node on a branch contains a disjunctive formula\vee
, then create two sibling children to the leaf of the branch, containing the formulaeA\veeB
andA
, respectively.B
This rule splits a branch into two, differing only for the final node. Since branches are considered in disjunction to each other, the two resulting branches are equivalent to the original one, as the disjunction of their non-common nodes is precisely
A\veeB
|
(\vee)
| A\veeB | |
| A\midB |
If nodes are assumed to contain sets of formulae, this rule is replaced by: if a node is labeled
Y\cup\{A\veeB\}
Y\cup\{A\}
Y\cup\{B\}
The aim of tableaux is to generate progressively simpler formulae until pairs of opposite literals are produced or no other rule can be applied. Negation can be treated by initially making formulae in negation normal form, so that negation only occurs in front of literals. Alternatively, one can use De Morgan's laws during the expansion of the tableau, so that for example
\neg(A\wedgeB)
\negA\vee\negB
\neg\negA
\neg\neg(A\wedgeB))
(\neg1)
| A | |
| \neg\negA |
(\neg2)
| \neg\negA | |
| A |
Every tableau can be considered as a graphical representation of a formula, which is equivalent to the set the tableau is built from. This formula is as follows: each branch of the tableau represents the conjunction of its formulae; the tableau represents the disjunction of its branches. The expansion rules transforms a tableau into one having an equivalent represented formula. Since the tableau is initialized as a single branch containing the formulae of the input set, all subsequent tableaux obtained from it represent formulae which are equivalent to that set (in the variant where the initial tableau is the single node labeled true, the formulae represented by tableaux are consequences of the original set.)
The method of tableaux works by starting with the initial set of formulae and then adding to the tableau simpler and simpler formulae until contradiction is shown in the simple form of opposite literals. Since the formula represented by a tableau is the disjunction of the formulae represented by its branches, contradiction is obtained when every branch contains a pair of opposite literals. Once a branch contains a literal and its negation, its corresponding formula is unsatisfiable. As a result, this branch can be now "closed", as there is no need to further expand it. If all branches of a tableau are closed, the formula represented by the tableau is unsatisfiable; therefore, the original set is unsatisfiable as well. Obtaining a tableau where all branches are closed is a way for proving the unsatisfiability of the original set. In the propositional case, one can also prove that satisfiability is proved by the impossibility of finding a closed tableau, provided that every expansion rule has been applied everywhere it could be applied. In particular, if a tableau contains some open (non-closed) branches and every formula that is not a literal has been used by a rule to generate a new node on every branch the formula is in, the set is satisfiable.
This rule takes into account that a formula may occur in more than one branch (this is the case if there is at least a branching point "below" the node). In this case, the rule for expanding the formula has to be applied so that its conclusion(s) are appended to all of these branches that are still open, before one can conclude that the tableau cannot be further expanded and that the formula is therefore satisfiable.
A variant of tableau is to label nodes with sets of formulae rather than single formulae. In this case, the initial tableau is a single node labeled with the set to be proved satisfiable. The formulae in a set are therefore considered to be in conjunction.
The rules of expansion of the tableau can now work on the leaves of the tableau, ignoring all internal nodes. For conjunction, the rule is based on the equivalence of a set containing a conjunction
A\wedgeB
A
B
X\cup\{A\wedgeB\}
X\cup\{A,B\}
(\wedge)
| X\cup\{A\wedgeB\ | |
For disjunction, a set
X\cup\{A\veeB\}
X\cup\{A\}
X\cup\{B\}
(\vee)
| X\cup\{A\veeB\ | |
Finally, if a set contains both a literal and its negation, this branch can be closed:
(id)
| X\cup\{p,\negp\ | |
A tableau for a given finite set X is a finite (upside down) tree with root X in which all child nodes are obtained by applying the tableau rules to their parents. A branch in such a tableau is closed if its leaf node contains "closed". A tableau is closed if all its branches are closed. A tableau is open if at least one branch is not closed.
Below are two closed tableaux for the set
X=\{r\wedge\negr, p\wedge((\negp\veeq)\wedge\negq)\}
\dfrac{ \dfrac{ r\wedge\negr, p\wedge((\negp\veeq)\wedge\negq) }{ r, \negr, p\wedge((\negp\veeq)\wedge\negq) }(\wedge) }{ closed }(\wedge)
\dfrac{ \dfrac{ \dfrac { r\wedge\negr, p\wedge((\negp\veeq)\wedge\negq) }{ r\wedge\negr, p, ((\negp\veeq)\wedge\negq) }(\wedge) }{ r\wedge\negr, p, (\negp\veeq), \negq }(\wedge) }{ \dfrac{ r\wedge\negr, p, \negp, \negq }{ closed }(id) \dfrac{ r\wedge\negr, p, q, \negq }{ closed }(id) }(\vee)
The first tableau closes after only one rule application while the second one misses the mark and takes a lot longer to close. Clearly, we would prefer to always find the shortest closed tableaux but it can be shown that one single algorithm that finds the shortest closed tableaux for all input sets of formulae cannot exist.
The three rules
(\wedge)
(\vee)
(id)
X'
Just apply all possible rules in all possible orders until we find a closed tableau forIn the first case,or until we exhaust all possibilities and conclude that every tableau forX'
is open.X'
X'
X'
X'
X'
These rules suffice for all of classical logic by taking an initial set of formulae X and replacing each member C by its logically equivalent negated normal form C' giving a set of formulae X' . We know that X is satisfiable if and only if X' issatisfiable, so it suffices to search for a closed tableau for X' using the procedure outlined above.
By setting
X=\{\negA\}
If the tableau forcloses then\{\negA\}
is unsatisfiable and so A is a tautology since no assignment of truth values will ever make A false. Otherwise any open leaf of any open branch of any open tableau for\negA
gives an assignment that falsifies A.\{\negA\}
Classical propositional logic usually has a connective to denote material implication. If we write this connective as ⇒, then the formula A ⇒ B stands for "if A then B". It is possible to give a tableau rule for breaking down A ⇒ B into its constituent formulae. Similarly, we can give one rule each for breaking down each of ¬(A ∧ B), ¬(A ∨ B), ¬(¬A), and ¬(A ⇒ B). Together these rules would give a terminating procedure for deciding whether a given set of formulae is simultaneously satisfiable in classical logic since each rule breaks down one formula into its constituents but no rule builds larger formulae out of smaller constituents. Thus we must eventually reach a node that contains only atoms and negations of atoms. If this last node matches (id) then we can close the branch, otherwise it remains open.
But note that the following equivalences hold in classical logic where (...) = (...) means that the left hand side formula is logically equivalent to the right hand side formula:
\begin{array}{lcl} \neg(A\landB)&=&\negA\lor\negB\\ \neg(A\lorB)&=&\negA\land\negB\\ \neg(\negA)&=&A\\ \neg(A ⇒ B)&=&A\land\negB\\ A ⇒ B&=&\negA\lorB\\ A\LeftrightarrowB&=&(A\landB)\lor(\negA\land\negB)\\ \neg(A\LeftrightarrowB)&=&(A\land\negB)\lor(\negA\landB) \end{array}
If we start with an arbitrary formula C of classical logic, and apply these equivalences repeatedly to replace the left hand sides with the right hand sides in C, then we will obtain a formula C' which is logically equivalent to C but which has the property that C' contains no implications, and ¬ appears in front of atomic formulae only. Such a formula is said to be in negation normal form and it is possible to prove formally that every formula C of classical logic has a logically equivalent formula C' in negation normal form. That is, C is satisfiable if and only if C' is satisfiable.
The above rules for propositional tableau can be simplified by using uniform notation. In uniform notation, each formula is either of type
\alpha
\beta
\alpha1,\alpha2
\beta1,\beta2
\alpha1
\alpha2
\alpha
\beta1
\beta2
\beta
\begin{array}{c|c|c}\alpha&\alpha1&\alpha2\ \hlineX\wedgeY&X&Y \ \neg(X\veeY)&\negX&\negY\ \neg(X\impliesY)&X&\negY\ \neg\negX&X&X\ \end{array}
\begin{array}{c|c|c}\beta&\beta1&\beta2\ \hline\neg(X\wedgeY)&\negX&\negY\ X\veeY&X&Y\ X\impliesY&\negX&Y\ \neg\negX&X&X\ \end{array}
In each table, the left-most column shows all the possible structures for the formulae of type alpha or beta, and the right-most columns show their respective components. Alternatively, the rules for uniform notation can be expressed using signed formulae:
\begin{array}{c|c|c}\alpha&\alpha1&\alpha2\ \hlineTX\wedgeY&TX&TY\ FX\veeY&FX&FY\ FX\impliesY&TX&FY\ F\negX&TX&TY\ T\negX&FX&FY\end{array} \begin{array}{c|c|c}\beta&\beta1&\beta2\ \hlineFX\wedgeY&FY&FX\ TX\veeY&TX&TY \ TX\impliesY&FX&TY\ F\negX&TX&TX\ T\negX&FX&FY\end{array}
When constructing a propositional tableau using the above notation, whenever one encounters a formula of type alpha, its two components
\alpha1,\alpha2
\theta
\theta
Tableaux are extended to first-order predicate logic by two rules for dealing with universal and existential quantifiers, respectively. Two different sets of rules can be used; both employ a form of Skolemization for handling existential quantifiers, but differ on the handling of universal quantifiers.
The set of formulae to check for validity is here supposed to contain no free variables; this is not a limitation as free variables are implicitly universally quantified, so universal quantifiers over these variables can be added, resulting in a formula with no free variables.
A first-order formula
\forallx.\gamma(x)
\gamma(t)
t
(\forall)
| \forallx.\gamma(x) | |
| \gamma(t) |
t
Contrarily to the rules for the propositional connectives, multiple applications of this rule to the same formula may be necessary. As an example, the set
\{\negP(a)\vee\negP(b),\forallx.P(x)\}
P(a)
P(b)
\forallx.P(x)
Existential quantifiers are dealt with by means of Skolemization. In particular, a formula with a leading existential quantifier like
\existsx.\delta(x)
\delta(c)
c
(\exists)
| \existsx.\delta(x) | |
| \delta(c) |
c
The Skolem term
c
x
x
The rule for existential quantifiers introduces new constant symbols. These symbols can be used by the rule for universal quantifiers, so that
\forally.\gamma(y)
\gamma(c)
c
The above two rules for universal and existential quantifiers are correct, and so are the propositional rules: if a set of formulae generates a closed tableau, this set is unsatisfiable. Completeness can also be proved: if a set of formulae is unsatisfiable, there exists a closed tableau built from it by these rules. However, actually finding such a closed tableau requires a suitable policy of application of rules. Otherwise, an unsatisfiable set can generate an infinite-growing tableau. As an example, the set
\{\negP(f(c)),\forallx.P(x)\}
\forallx.P(x)
P(c),P(f(c)),P(f(f(c))),\ldots
The rule for universal quantifiers
(\forall)
The main problem of tableau without unification is how to choose a ground term
t
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. This can be done by using a variable instead of a term, so that
\forallx.\gamma(x)
\gamma(x')
x'
(\forall)
| \forallx.\gamma(x) | |
| \gamma(x') |
x'
While the initial set of formulae is supposed not to contain free variables, a formula of the tableau may contain the free variables generated by this rule. These free variables are implicitly considered universally quantified.
This rule employs a variable instead of a ground term. 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.
(\sigma) | if \sigma A B A B \sigma |
As an example,
\{\negP(a),\forallx.P(x)\}
P(x1)
\negP(a)
x1
a
P(x1)
P(a)
Existential quantifiers are dealt with by Skolemization. Contrary to the tableau without unification, Skolem terms may not be simple constants. Indeed, formulae in a tableau with unification may contain free variables, which are implicitly considered universally quantified. As a result, a formula like
\existsx.\delta(x)
(\exists)
| \existsx.\delta(x) | |
| \delta(f(x1,\ldots,xn)) |
f
x1,\ldots,xn
\delta
This rule incorporates a simplification over a rule where
x1,\ldots,xn
\delta
\delta
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. As for the propositional case, formulae in each branch are conjoined and the resulting formulae are disjoined. In addition, all free variables of the resulting formula are universally quantified. All these quantifiers have the whole formula in their scope. In other words, if
F
x1,\ldots,xn
\forallx1,\ldots,xn.F
\gamma(x')
\gamma
x'
\gamma(t)
t
x
A(x)
B(x)
x
\forallx.(...A(x)...B(x)...)
(...A(x)...B(x)...)
x
(...A(t)...A(t')...)
t
t'
x
A(x)
B(x)
P(x) → P(c)
D=\{1,2\},P(1)=\bot,P(2)=\top,c=1
x=2
\{P(x),\negP(c)\}
P(x)
\negP(c)
x
c
\forallx.(P(x) → P(c))
The following two variants are also correct.
Tableaux with unification can be proved complete: if a set of formulae is unsatisfiable, it has a tableau-with-unification proof. However, actually finding such a proof may be a difficult problem. Contrarily to the case without unification, applying a substitution can modify the existing part of a tableau; while applying a substitution closes at least a branch, it may make other branches impossible to close (even if the set is unsatisfiable).
A solution to this problem is delayed instantiation: no substitution is applied until one that closes all branches at the same time is found. With this variant, a proof for an unsatisfiable set can always be found by a suitable policy of application of the other rules. This method however requires the whole tableau to be kept in memory: the general method closes branches, which can be then discarded, while this variant does not close any branch until the end.
The problem that some tableaux that can be generated are impossible to close even if the set is unsatisfiable is common to other sets of tableau expansion rules: even if some specific sequences of application of these rules allow constructing a closed tableau (if the set is unsatisfiable), some other sequences lead to tableaux that cannot be closed. General solutions for these cases are outlined in the "Searching for a tableau" section.
A tableau calculus is a set of rules that allows building and modification of a tableau. Propositional tableau rules, tableau rules without unification, and tableau rules with unification, are all tableau calculi. Some important properties a tableau calculus may or may not possess are completeness, destructiveness, and proof confluence.
A tableau calculus is called complete if it allows building a tableau proof for every given unsatisfiable set of formulae. The tableau calculi mentioned above can be proved complete.
A remarkable difference between tableau with unification and the other two calculi is that the latter two calculi only modify a tableau by adding new nodes to it, while the former one allows substitutions to modify the existing part of the tableau. More generally, tableau calculi are classed as destructive or non-destructive depending on whether they only add new nodes to tableau or not. Tableau with unification is therefore destructive, while propositional tableau and tableau without unification are non-destructive.
Proof confluence is the property of a tableau calculus being able to obtain a proof for an arbitrary unsatisfiable set from an arbitrary tableau, assuming that this tableau has itself been obtained by applying the rules of the calculus. In other words, in a proof confluent tableau calculus, from an unsatisfiable set one can apply whatever set of rules and still obtain a tableau from which a closed one can be obtained by applying some other rules.
A tableau calculus is simply a set of rules that prescribes how a tableau can be modified. A proof procedure is a method for actually finding a proof (if one exists). In other words, a tableau calculus is a set of rules, while a proof procedure is a policy of application of these rules. Even if a calculus is complete, not every possible choice of application of rules leads to a proof of an unsatisfiable set. For example,
\{P(f(c)),R(c),\negP(f(c))\vee\negR(c),\forallx.Q(x)\}
Propositional tableaux and tableaux without unification have strongly complete proof procedures. In particular, a complete proof procedure is that of applying the rules in a fair way. This is because the only way such calculi cannot generate a closed tableau from an unsatisfiable set is by not applying some applicable rules.
For propositional tableaux, fairness amounts to expanding every formula in every branch. More precisely, for every formula and every branch the formula is in, the rule having the formula as a precondition has been used to expand the branch. A fair proof procedure for propositional tableaux is strongly complete.
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. Fairness amounts to expanding every universal quantifier infinitely often. In other words, a fair policy of application of rules cannot keep applying other rules without expanding every universal quantifier in every branch that is still open once in a while.
If a tableau calculus is complete, every unsatisfiable set of formulae has an associated closed tableau. While this tableau can always be obtained by applying some of the rules of the calculus, the problem of which rules to apply for a given formula still remains. 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. While a fair proof procedure is complete for ground tableau and tableau without unification, this is not the case for tableau with unification.
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). In this approach, one starts with an empty tableau and then recursively applies every possible applicable rule. This procedure visits a (implicit) tree whose nodes are labeled with tableaux, and such that the tableau in a node is obtained from the tableau in its parent by applying one of the valid rules.
Since each branch can be infinite, this tree has to be visited breadth-first rather than depth-first. This requires a large amount of space, as the breadth of the tree can grow exponentially. A method that may visit some nodes more than once but works in polynomial space is to visit in a depth-first manner with iterative deepening: one first visits the tree depth first up to a certain depth, then increases the depth and perform the visit again. This particular procedure uses the depth (which is also the number of tableau rules that have been applied) for deciding when to stop at each step. Various other parameters (such as the size of the tableau labeling a node) have been used instead.
The size of the search tree depends on the number of (children) tableaux that can be generated from a given (parent) one. Reducing the number of such tableaux therefore reduces the required search.
A way for reducing this number is to disallow the generation of some tableaux based on their internal structure. An example is the condition of regularity: if a branch contains a literal, using an expansion rule that generates the same literal is useless because the branch containing two copies of the literals would have the same set of formulae of the original one. This expansion can be disallowed because if a closed tableau exists, it can be found without it. This restriction is structural because it can be checked by looking at the structure of the tableau to expand only. 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. These restrictions are called global. As an example of a global restriction, one may employ a rule that specifies which of the open branches is to be expanded. As a result, if a tableau has for example two non-closed branches, the rule specifies which one is to be expanded, disallowing the expansion of the second one. 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. As an example, a tableau with root
\nega\wedge\negb
a\veeb
a
b
(\wedge)
a
b
(\wedge)
a
b
a
b
When applied to sets of clauses (rather than of arbitrary formulae), tableaux methods allow for a number of efficiency improvements. A first-order clause is a formula
\forallx1,\ldots,xnL1\vee … \veeLm
Li
P(x,y)\veeQ(f(x))
\forallx,y.P(x,y)\veeQ(f(x))
P(x,y)\veeQ(f(x))
\existsx,y.P(x,y)\veeQ(f(x))
The only expansion rules that are applicable to a clause are
(\forall)
(\vee)
(\forall)
(\vee)
(C)
| L1\vee … \veeLn | |
| L1'| … |Ln' |
L1'\vee … \veeLn'
L1\vee … \veeLn
When the set to be checked for satisfiability is only composed of clauses, this and the unification rules are sufficient to prove unsatisfiability. In other worlds, the tableau calculi composed of
(C)
(\sigma)
Since the clause expansion rule only generates literals and never new clauses, the clauses to which it can be applied are only clauses of the input set. As a result, the clause expansion rule can be further restricted to the case where the clause is in the input set.
(C)
| L1\vee … \veeLn | |
| L1'| … |Ln' |
L1'\vee … \veeLn'
L1\vee … \veeLn
Since this rule directly exploits the clauses in the input set there is no need to initialize the tableau to the chain of the input clauses. The initial tableau can therefore be initialize with the single node labeled
true
Connection is a condition over tableau that forbids expanding a branch using clauses that are unrelated to the literals that are already in the branch. Connection can be defined in two ways:
Both conditions apply only to branches consisting not only of the root. The second definition allows for the use of a clause containing a literal that unifies with the negation of a literal in the branch, while the first only further constraint that literal to be in leaf of the current branch.
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. In particular, this is the leaf containing the literal of the clause that unifies with the negation of a literal in the branch (or the negation of the literal in the parent, in case of strong connection).
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. Such a closed tableau can be found by searching in the space of tableaux as explained in the "Searching for a closed tableau" section. During this search, connectedness eliminates some possible choices of expansion, thus reducing search. In other worlds, while the tableau in a node of the tree can be in general expanded in several different ways, connection may allow only few of them, thus reducing the number of resulting tableaux that need to be further expanded.
This can be seen on the following (propositional) example. The tableau made of a chain
true-a
\{a,\nega\veeb,\negc\veed,\negb\}
\nega\veeb
The connectedness conditions, when applied to the propositional (clausal) case, make the resulting calculus non-confluent. As an example,
\{a,b,\negb\}
(C)
a
true-a
A tableau is regular if no literal occurs twice in the same branch. Enforcing this condition allows for a reduction of the possible choices of tableau expansion, as the clauses that would generate a non-regular tableau cannot be expanded.
These disallowed expansion steps are however useless. If
B
L
C
C
L
B-L
L
B
B-L
B
C
C
In a modal logic, a model comprises a set of possible worlds, each one associated to a truth evaluation; an accessibility relation specifies when a world is accessible from another one. A modal formula may specify not only conditions over a possible world, but also on the ones that are accessible from it. As an example,
\BoxA
A
As for propositional logic, tableaux for modal logics are based on recursively breaking formulae into its basic components. Expanding a modal formula may however require stating conditions over different worlds. As an example, if
\neg\BoxA
A
| \neg\BoxA | |
| \negA |
In propositional tableaux all formulae refer to the same truth evaluation, but the precondition of the rule above holds in one world while the consequence holds in another. Not taking this into account would generate incorrect results. For example, formula
a\wedge\neg\Boxa
a
a
(\wedge)
a
\nega
Technically, tableaux for modal logics check the satisfiability of a set of formulae: they check whether there exists a model
M
w
a
a
w
\neg\Boxa
\nega
w'
w
w
This fact has an important consequence: formulae that hold in a world may imply conditions over different successors of that world. Unsatisfiability may then be proved from the subset of formulae referring to a single successor. This holds if a world may have more than one successor, which is true for most modal logics. If this is the case, a formula like
\neg\BoxA\wedge\neg\BoxB
\negA
\negB
\negA
\negB
\negB
\negA
\neg\BoxA\wedge\neg\BoxB
\negA
\negB
\neg\BoxA
\neg\BoxB
Depending on whether the precondition and consequence of a tableau expansion rule refer to the same world or not, the rule is called static or transactional. While rules for propositional connectives are all static, not all rules for modal connectives are transactional: for example, in every modal logic including axiom T, it holds that
\BoxA
A
A method for avoiding formulae referring to different worlds interacting in the wrong way is to make sure that all formulae of a branch 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. When expanding a branch, two situations are possible: either the new formulae refer to the same world as the other one in the branch or not. In the first case, the rule is applied normally. In the second case, all formulae of the branch that do not also hold in the new world are deleted from the branch, and possibly added to all other branches that are still relative to the old world.
As an example, in S5 every formula
\BoxA
A
\BoxA
| \neg\BoxB | |
| \negB |
\BoxA
A different mechanism for ensuring the correct interaction between formulae referring to different worlds is to switch from formulae to labeled formulae: instead of writing
A
w:A
A
w
All propositional expansion rules are adapted to this variant by stating that they all refer to formulae with the same world label. For example,
w:A\wedgeB
w:A
w:B
w:a
w:\nega
w:a
w':\nega
A modal expansion rule may have a consequence that refers to different worlds. For example, the rule for
\neg\BoxA
| w:\neg\BoxA | |
| w':\negA |
The precondition and consequent of this rule refer to worlds
w
w'
wRw'
w'
w
(1,4,2,3)
(1,4,2)
The problem of interaction between formulae holding in different worlds can be overcome by using set-labeling tableaux. These are trees whose nodes are labeled with sets of formulae; the expansion rules explain how to attach new nodes to a leaf, based only on the label of the leaf (and not on the label of other nodes in the branch).
Tableaux for modal logics are used to verify the satisfiability of a set of modal formulae in a given modal logic. Given a set of formulae
S
M
w
M,w\modelsS
The expansion rules depend on the particular modal logic used. A tableau system for the basic modal logic K can be obtained by adding to the propositional tableau rules the following one:
(K)
| \BoxA1;\ldots;\BoxAn;\neg\BoxB | |
| A1;\ldots;An;\negB |
Intuitively, the precondition of this rule expresses the truth of all formulae
A1,\ldots,An
\negB
\negB
More technically, modal tableaux methods check the existence of a model
M
w
\BoxA1;\ldots;\BoxAn;\neg\BoxB
w
w'
w
A1;\ldots;An;\negB
w'
While the preconditions
\BoxA1;\ldots;\BoxAn;\neg\BoxB
M,w
A1;\ldots;An;\negB
M,w'
As a result of the possibly different worlds where formulae are assumed true, a formula in a node is not automatically valid in all its descendants, as every application of the modal rule corresponds to a move from a world to another one. 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.
Notably,
(K)
\BoxA1;\ldots;\BoxAn;\neg\BoxB1;\neg\BoxB2
B1
B2
Differently from the propositional rules,
(K)
a;\Boxb;\Box(b → c);\neg\Boxc
(K)
a
(\theta)
| A1;\ldots;An;B1;\ldots;Bm | |
| A1;\ldots;An |
The addition of this rule (thinning rule) makes the resulting calculus non-confluent: a tableau for an inconsistent set may be impossible to close, even if a closed tableau for the same set exists.
Rule
(\theta)
This non-determinism can be avoided by restricting the usage of
(\theta)
(\theta)
Axiom T expresses reflexivity of the accessibility relation: every world is accessible from itself. The corresponding tableau expansion rule is:
(T)
| A1;\ldots;An;\BoxB | |
| A1;\ldots;An;\BoxB;B |
This rule relates conditions over the same world: if
\BoxB
B
This rule copies
\BoxB
B
\BoxB
\Box(a\wedge\neg\Boxa)
(T),(\wedge),(\theta),(K)
\Boxa
A different method for dealing with formulae holding in alternate worlds is to start a different tableau for each new world that is introduced in the tableau. For example,
\neg\BoxA
A
\negA
The above modal tableaux establish the consistency of a set of formulae, and can be used for solving the local logical consequence problem. This is the problem of telling whether, for each model
M
A
w
B
B
A
A related problem is the global consequence problem, where the assumption is that a formula (or set of formulae)
G
M
G
B
Local and global assumption differ on models where the assumed formula is true in some worlds but not in others. As an example,
\{P,\neg\Box(P\wedgeQ)\}
\neg\BoxQ
P
\negP,Q
\neg\BoxQ
P
\negP
These two problems can be combined, so that one can check whether
B
A
G
The following conventions are sometimes used.
When writing tableaux expansion rules, formulae are often denoted using a convention, so that for example
\alpha
\alpha1\wedge\alpha2
\alpha | \alpha1\wedge\alpha2 | \neg(\overline{\alpha1}\vee\overline{\alpha2}) | \neg(\alpha1 → \overline{\alpha2}) |
\beta | \beta1\vee\beta2 | \overline{\beta1} → \beta2 | \neg(\overline{\beta1}\wedge\overline{\beta2}) |
\gamma | \forallx\gamma1(x) | \neg\existsx\overline{\gamma1(x)} | |
\delta | \existsx\delta1(x) | \neg\forallx\overline{\delta1(x)} | |
\pi | \Diamond\pi1 | \neg\Box\overline{\pi1} | |
\nu | \Box\nu1 | \neg\Diamond\overline{\nu1} |
Each label in the first column is taken to be either formula in the other columns. An overlined formula such as
\overline{\alpha1}
\alpha1
\neg(a\veeb)
\alpha1
a
Since every label indicates many equivalent formulae, this notation allows writing a single rule for all these equivalent formulae. For example, the conjunction expansion rule is formulated as:
(\alpha)
| \alpha | |
| \begin{array |
{c}\alpha1\ \alpha2\end{array}}
A formula in a tableau is assumed true. Signed tableaux allows stating that a formula is false. This is generally achieved by adding a label to each formula, where the label T indicates formulae assumed true and F those assumed false. A different but equivalent notation is that to write formulae that are assumed true at the left of the node and formulae assumed false at its right.
\top
\{(a\vee\negb)\wedgeb,\nega\}