Clause Tableaux
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 that does not contain free variables and such that each is a literal. The universal quantifiers are often omitted for clarity, so that for example actually means . Note that, if taken literally, these two formulae are not the same as for satisfiability: rather, the satisfiability is the same as that of . 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.
The only expansion rules that are applicable to a clause are and ; these two rules can be replaced by their combination without losing completeness. In particular, the following rule corresponds to applying in sequence the rules and of the first-order calculus with unification.
- where is obtained by replacing every variable with a new one in
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 and is complete.
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.
- where is obtained by replacing every variable with a
new one in, which is a clause of the input set
Since this rule directly exploit 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 ; this label is often omitted as implicit. As a result of this further simplification, every node of the tableau (apart of the root) is labeled with a literal.
A number of optimizations can be used for clause tableau. These optimization are aimed at reducing the number of possible tableaux to be explored when searching for a closed tableau as described in the "Searching for a closed tableau" section above.
Read more about this topic: Method Of Analytic Tableaux
Famous quotes containing the word clause:
“Long ago I added to the true old adage of “What is everybody’s business is nobody’s business,” another clause which, I think, more than any other principle has served to influence my actions in life. That is, What is nobody’s business is my business.”
—Clara Barton (1821–1912)