Proof Procedures
A tableau calculus is simply a set of rules that tells 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 quantifier 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.
Read more about this topic: Method Of Analytic Tableaux
Famous quotes containing the words proof and/or procedures:
“The thing with Catholicism, the same as all religions, is that it teaches what should be, which seems rather incorrect. This is “what should be.” Now, if you’re taught to live up to a “what should be” that never existed—only an occult superstition, no proof of this “should be”Mthen you can sit on a jury and indict easily, you can cast the first stone, you can burn Adolf Eichmann, like that!”
—Lenny Bruce (1925–1966)
“Young children learn in a different manner from that of older children and adults, yet we can teach them many things if we adapt our materials and mode of instruction to their level of ability. But we miseducate young children when we assume that their learning abilities are comparable to those of older children and that they can be taught with materials and with the same instructional procedures appropriate to school-age children.”
—David Elkind (20th century)