0
$\begingroup$

When I use the resolution "tree" to determine whether formula is satisfiable, it gives me wrong result: enter image description here

Can you find my mistake and explain how is it done right?

Grant

1 Answers 1

0

You can resolve something of the form $(X\lor Y)\land (\lnot X \lor Z)$ to $(Y\lor Z)$.

You did the first resolution correctly, resolving $(\lnot A \lor B) \land (\lnot B \lor C)$ to $(\lnot A \lor C)$. But you skipped a step in the second resolution. You should have resolved $(\lnot A\lor C) \land (\lnot C\lor A)$ to $(C \lor \lnot C)$, which is $\top$, but instead you resolved it to $\bot$.

  • 1
    You can, but the result of crossing them all out is $\top$, not $\bot$, because you are crossing them out from a conjunction, and an empty conjunction is true, not false.2012-12-30