I have to do different exercises concerning the tableau method. So for example I need to show if a formula $X$ is tautology or not. So I have to check if all branches of $\neg X$ are closed right? But what do I do if the branches do not close? Have I found a boolean assignment such that $X$ is false?
And I also have a different kind of exercise with not one formula, but a set of formulas, so do i have to negate all of them and use the tableau method again?
I am really confused right now and would appreciate any help!
1 Answer
$\begingroup$Correct.
The tableau method is a refutation procedure; if all the branches of the tableau close, then the initial formula is unsatisfiable.
Thus, if we start with $\lnot X$ and the tableau closes, this means that $\lnot X$ is unsatisfiable, i.e. $X$ is a tauitology.
If the procedure ends and a branch does not close, this branch determines an assignment of truth values to the atoms that satisfy the initial formula: in our case $\lnot X$.
But if $\lnot X$ is satisfied by a suitable assignment, this means that, for that assignment, $X$ is falsified, and so $X$ is not a tautology.
With a set of formulas, we can have two types of question:
(i) to check if the last one (the conclusion) is implied by the others (the premise).
In this case, we have to consider the premises with the negation of the conclusion; if the tableau closes, this fact proves that the conclusion is impklied by the premises.
(ii) to check if the set of formulas is satisfiable.
In this case we apply the tableau to the original set of formulas; if the tableau is opne, this means that the set of formulas is satisfiable.
$\endgroup$ 3
