Introduction
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 evidentPropositional logic
This section presents the tableau calculus for classical propositional logic. 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 imply if is unsatisfiable. 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.And
() If a branch of the tableau contains a conjunctive formula , add to its leaf the chain of two nodes containing the formulae andThis rule is generally written as follows: : 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 at the end of a branch containing . More precisely, if a node on a branch is labeled , one can add to the branch the new leaf .
Or
() If a node on a branch contains a disjunctive formula , then create two sibling children to the leaf of the branch, containing the formulae and , respectively.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 . The rule for disjunction is generally formally written using the symbol for separating the formulae of the two distinct nodes to be created: : If nodes are assumed to contain sets of formulae, this rule is replaced by: if a node is labeled , a leaf of the branch this node is in can be appended two sibling child nodes labeled and , respectively.
Not
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 useClosure
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.)Set-labeled tableau
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 with the set containing both and in place of it. In particular, if a leaf is labeled with , a node can be appended to it with label : : For disjunction, a set is equivalent to the disjunction of the two sets and . As a result, if the first set labels a leaf, two children can be appended to it, labeled with the latter two formulae. : Finally, if a set contains both a literal and its negation, this branch can be closed: : 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. Here are two closed tableaux for the set ''X'' = with each rule application marked at the right hand side (& and ~ stand for and , respectively) --------------------------------------(&) ------------------------------------------------------------(&) -------------------------------------(id) ----------------------------------------------------------(&) closed -------------------------------------------------------------(v) , -------------------------- (id) ---------------------- (id) closed closed The left hand tableau closes after only one rule application while the right hand 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 , and given above are then enough to decide if a given set of formulae in negated normal form are jointly satisfiable:Just apply all possible rules in all possible orders until we find a closed tableau for or until we exhaust all possibilities and conclude that every tableau for is open.In the first case, is jointly unsatisfiable and in the second the case the leaf node of the open branch gives an assignment to the atomic formulae and negated atomic formulae which makes jointly satisfiable. Classical logic actually has the rather nice property that we need to investigate only (any) one tableau completely: if it closes then is unsatisfiable and if it is open then is satisfiable. But this property is not generally enjoyed by other logics. 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' '' is satisfiable, so it suffices to search for a closed tableau for ''X' '' using the procedure outlined above. By setting we can test whether the formula ''A'' is a tautology of classical logic:
If the tableau for closes then is unsatisfiable and so ''A'' is a tautology since no assignment oftruth value In logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth, which in classical logic has only two possible values ('' true'' or ''false''). Computing In some prog ...s will ever make ''A'' false. Otherwise any open leaf of any open branch of any open tableau for gives an assignment that falsifies ''A''.
Conditional
ClassicalFirst-order logic tableau
Tableaux are extended toFirst-order tableau without unification
A first-order formula implies all formulae where is aFirst-order tableau with unification
The main problem of tableau without unification is how to choose a ground term for the universal quantifier rule. Indeed, every possible ground term can be used, but clearly most of them might be useless for closing the tableau. 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 generates , and then allowing substitutions to later replace with a term. The rule for universal quantifiers becomes: : where is a variable not occurring everywhere else in the tableau 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. : As an example, can be proved unsatisfiable by first generating ; the negation of this literal is unifiable with , the most general unifier being the substitution that replaces with ; applying this substitution results in replacing with , which closes the tableau. This rule closes at least a branch of the tableau—the one containing the considered pair of literals. However, the substitution has to be applied to the whole tableau, not only on these two literals. This is expressed by saying that the free variables of the tableau are ''rigid'': if an occurrence of a variable is replaced by something else, all other occurrences of the same variable must be replaced in the same way. Formally, the free variables are (implicitly) universally quantified and all formulae of the tableau are within the scope of these quantifiers. 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 may be within the scope of universal quantifiers; if this is the case, theTableau calculi and their properties
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.Proof procedures
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, is unsatisfiable, but both tableaux with unification and tableaux without unification allow the rule for the universal quantifiers to be applied repeatedly to the last formula, while simply applying the rule for disjunction to the third one would directly lead to closure. For proof procedures, a definition of completeness has been given: a proof procedure is strongly complete if it allows finding a closed tableau for any given unsatisfiable set of formulae. Proof confluence of the underlying calculus is relevant to completeness: proof confluence is the guarantee that a closed tableau can be always generated from an arbitrary partially constructed tableau (if the set is unsatisfiable). Without proof confluence, the application of a 'wrong' rule may result in the impossibility of making the tableau complete by applying other rules. 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.Searching for a closed tableau
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.Reducing search
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 , child , and two leaves and can be closed in two ways: applying first to and then to , or vice versa. There is clearly no need to follow both possibilities; one may consider only the case in which is first applied to and disregard the case in which it is first applied to . This is a global restriction because what allows neglecting this second expansion is the presence of the other tableau, where expansion is applied to first and afterwards.Clause tableaux
When applied to sets ofConnection tableau
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: ; strong connectedness : when expanding a branch, use an input clause only if it contains a literal that can be unified with the negation of the literal in the current leaf ; weak connectedness : allow the use of clauses that contain a literal that unifies with the negation of a literal on the branch 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 for the set of clauses can be in general expanded using each of the four input clauses, but connection only allows the expansion that uses . This means that the tree of tableaux has four leaves in general but only one if connectedness is imposed. This means that connectedness leaves only one tableau to try to expand, instead of the four ones to consider in general. 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. As an example, is unsatisfiable, but applying to generates the chain , which is not closed and to which no other expansion rule can be applied without violating either strong or weak connectedness. In the case of weak connectedness, confluence holds provided that the clause used for expanding the root is relevant to unsatisfiability, that is, it is contained in a minimally unsatisfiable subset of the set of clauses. Unfortunately, the problem of checking whether a clause meets this condition is itself a hard problem. In spite of non-confluence, a closed tableau can be found using search, as presented in the "Searching for a closed tableau" section above. While search is made necessary, connectedness reduces the possible choices of expansion, thus making search more efficient.Regular tableaux
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 is a branch containing a literal , and is a clause whose expansion violates regularity, then contains . In order to close the tableau, one needs to expand and close, among others, the branch where , where occurs twice. However, the formulae in this branch are exactly the same as the formulae of alone. As a result, the same expansion steps that close also close . This means that expanding was unnecessary; moreover, if contained other literals, its expansion generated other leaves that needed to be closed. In the propositional case, the expansion needed to close these leaves are completely useless; in the first-order case, they may only affect the rest of the tableau because of some unifications; these can however be combined to the substitutions used to close the rest of the tableau.Tableaux for modal logics
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, is true in a world if is true in all worlds that are accessible from it. 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 is true in a world then there exists a world accessible from it where is false. However, one cannot simply add the following rule to the propositional ones. : 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 into account this would generate incorrect results. For example, formula states that is true in the current world and is false in a world that is accessible from it. Simply applying and the expansion rule above would produce and , but these two formulae should not in general generate a contradiction, as they hold in different worlds. 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. Technically, tableaux for modal logics check the satisfiability of a set of formulae: they check whether there exists a model and world such that the formulae in the set are true in that model and world. In the example above, while states the truth of in , the formula states the truth of in some world that is accessible from and which may in general be different from . Tableaux calculi for modal logic take into account that formulae may refer to different worlds. 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 is true if a successor where holds exists and a successor where holds exists. In the other way around, if one can show unsatisfiability of in an arbitrary successor, the formula is proved unsatisfiable without checking for worlds where holds. At the same time, if one can show unsatisfiability of , there is no need to check . As a result, while there are two possible way to expand , one of these two ways is always sufficient to prove unsatisfiability if the formula is unsatisfiable. For example, one may expand the tableau by considering an arbitrary world where holds. If this expansion leads to unsatisfiability, the original formula is unsatisfiable. However, it is also possible that unsatisfiability cannot be proved this way, and that the world where holds should have been considered instead. As a result, one can always prove unsatisfiability by expanding either only or only; however, if the wrong choice is made the resulting tableau may not be closed. Expanding either subformula leads to tableau calculi that are complete but not proof-confluent. Searching as described in the "Searching for a closed tableau" may therefore be necessary. 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 implies in the same world. As a result, the relative (modal) tableau expansion rule is static, as both its precondition and consequence refer to the same world.Formula-deleting tableau
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 that is true in a world is also true in all accessible worlds (that is, in all accessible worlds both and are true). Therefore, when applying , whose consequence holds in a different world, one deletes all formulae from the branch, but can keep all formulae , as these hold in the new world as well. In order to retain completeness, the deleted formulae are then added to all other branches that still refer to the old world.World-labeled tableau
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 , one would write to make it explicit that holds in world . All propositional expansion rules are adapted to this variant by stating that they all refer to formulae with the same world label. For example, generates two nodes labeled with and ; a branch is closed only if it contains two opposite literals of the same world, like and ; no closure is generated if the two world labels are different, like in and . A modal expansion rule may have a consequence that refers to different worlds. For example, the rule for would be written as follows : The precondition and consequent of this rule refer to worlds and , respectively. The various calculi use different methods for keeping track of the accessibility of the worlds used as labels. Some include pseudo-formulae like to denote that is accessible from . Some others use sequences of integers as world labels, this notation implicitly representing the accessibility relation (for example, is accessible from .)Set-labeling tableaux
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 , they check the existence of a model and a world such that . 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: : Intuitively, the precondition of this rule expresses the truth of all formulae at all accessible worlds, and truth of at some accessible worlds. The consequence of this rule is a formula that must be true at one of those worlds where is true. More technically, modal tableaux methods check the existence of a model and a world that make set of formulae true. If are true in , there must be a world that is accessible from and that makes true. This rule therefore amounts to deriving a set of formulae that must be satisfied in such . While the preconditions are assumed satisfied by , the consequences are assumed satisfied in : same model but possibly different worlds. Set-labeled tableaux do not explicitly keep track of the world where each formula is assumed true: two nodes may or may not refer to the same world. However, the formulae labeling any given node are assumed true at the same world. 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, does not directly extend to multiple negated boxed formulae such as in : while there exists an accessible world where is false and one in which is false, these two worlds are not necessarily the same. Differently from the propositional rules, states conditions over all its preconditions. For example, it cannot be applied to a node labeled by ; while this set is inconsistent and this could be easily proved by applying , this rule cannot be applied because of formula , which is not even relevant to inconsistency. Removal of such formulae is made possible by the rule: : 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 is non-deterministic: the set of formulae to be removed (or to be kept) can be chosen arbitrarily; this creates the problem of choosing a set of formulae to discard that is not so large it makes the resulting set satisfiable and not so small it makes the necessary expansion rules inapplicable. Having a large number of possible choices makes the problem of searching for a closed tableau harder. This non-determinism can be avoided by restricting the usage of so that it is only applied before a modal expansion rule, and so that it only removes the formulae that make that other rule inapplicable. This condition can be also formulated by merging the two rules in a single one. The resulting rule produces the same result as the old one, but implicitly discard all formulae that made the old rule inapplicable. This mechanism for removing has been proved to preserve completeness for many modal logics. Axiom T expresses reflexivity of the accessibility relation: every world is accessible from itself. The corresponding tableau expansion rule is: : This rule relates conditions over the same world: if is true in a world, by reflexivity is also true ''in the same world''. This rule is static, not transactional, as both its precondition and consequent refer to the same world. This rule copies from the precondition to the consequent, in spite of this formula having been "used" to generate . This is correct, as the considered world is the same, so also holds there. This "copying" is necessary in some cases. It is for example necessary to prove the inconsistency of : the only applicable rules are in order , from which one is blocked if is not copied.Auxiliary tableaux
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, implies that is false in an accessible world, so one starts a new tableau rooted by . This new tableau is attached to the node of the original tableau where the expansion rule has been applied; a closure of this tableau immediately generates a closure of all branches where that node is, regardless of whether the same node is associated other auxiliary tableaux. The expansion rules for the auxiliary tableaux are the same as for the original one; therefore, an auxiliary tableau can have in turns other (sub-)auxiliary tableaux.Global assumptions
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 , if is true in a world , then is also true in the same world. This is the same as checking whether is true in a world of a model, in the assumption that is also true in the same world of the same model. A related problem is the global consequence problem, where the assumption is that a formula (or set of formulae) is true in all possible worlds of the model. The problem is that of checking whether, in all models where is true in all worlds, is also true in all worlds. Local and global assumption differ on models where the assumed formula is true in some worlds but not in others. As an example, entails globally but not locally. LocalNotations
The following conventions are sometimes used.Uniform notation
When writing tableaux expansion rules, formulae are often denoted using a convention, so that for example is always considered to be . The following table provides the notation for formulae in propositional, first-order, and modal logic. Each label in the first column is taken to be either formula in the other columns. An overlined formula such as indicates that is the negation of whatever formula appears in its place, so that for example in formula the subformula is the negation of . 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: :Signed formulae
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.History
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 logicianSee also
*References
* Reprinted in * * * * * * * * * *{{cite book , first=Joseph Jay , last=Zeman , title=Modal Logic: The Lewis-modal Systems , publisher=Clarendon Press , date=1973 , isbn=978-0-19-824374-8 , oclc=641504 , url=http://www.clas.ufl.edu/users/jzeman/modallogic/External links