Sample Decision Procedure

The tableau decision procedure for classical propositional formulas is especially well understood (and still current, see the account in [40]). The idea is that given a formula, we try to systematically falsify it by building up a truth assignment to the subformulas, eventually including the atomic ones (the variables). If we succeed, then the formula is not a tautology as the falsifying assignment attests. If we fail in this systematic attempt, then we can show that the resulting formula is valid and has a propositional proof, that is, one using only rules of the propositional calculus. To illustrate, consider the following formula.

Decision Procedure

Show that

$$((A\Rightarrow B_1) \; \& \; (B_1\Rightarrow B_2) \; \& \; (B_2\Rightarrow B_3))\Rightarrow(A\Rightarrow B_3)$$

is a tautology.

Try to assign it the truth-value F

$$\mbox{\boldmath$T$}(A\Rightarrow B_1 \; \& \; B_1\Rightarrow B_2 \; \& \; B_2\Rightarrow B_3) \mbox{\boldmath $F$}(A\Rightarrow B_3)$$

Now force the assignment to the other atoms in the natural way:

$$\mbox{\boldmath$T$}(A\Rightarrow B_1)$$

Now consider these observations.