I was referring to this MIT OCW slides to learn about resolution refutation.
Recently I came across following problem:
Check if following is tautology
$(a\leftrightarrow c)\rightarrow (\lnot b\rightarrow (a\land c))$
I tried solving like this:
$= (a∨¬c)∧(c∨¬a)$…this is CNF
$=¬b∧(¬b∨¬a)∧(¬c∨¬b)∧(¬c∨¬a)$ …this is CNF
Then applied resolution refutation as follows:
I am not able to reduce this to false, so I can say that the contradiction is true and the statement is not a tautology. Am I correct with this? Also I have following doubts
The examples in the slides explains examples which involve single variable conclusions (like $Z$ and $P$), but not compound expressions involving as in case of above. So did I handled conclusion involving compound expression above correctly?
Is it correct to use the expansion of biconditional as in case of premise ($a\leftrightarrow c$) above?
The slides says that we can bring FALSE after applying resolution inference rule, it means the contradiction is false and the original statement is valid. But, the slides does not explain what to conclude if we can bring TRUE after applying resolution rule, does it mean that the contradiction is true? And hence the given statement if invalid / not tautology.
Above by applying resolution inference rule to point (1) and (2), I can get TRUE, right? $(a\vee\neg c)\wedge(\neg a\vee c) = (\neg a\to \neg c)\wedge(\neg c\to \neg a)=(\neg a\to \neg a)=a\vee \neg a=TRUE$
If yes, then the next question.
- Does that mean all premises involving biconditional (above TRUE is obtained from biconditional premise expressed as conjunction) leads to correct contradiction?