When I use the resolution "tree" to determine whether formula is satisfiable, it gives me wrong result:
Can you find my mistake and explain how is it done right?
Grant
When I use the resolution "tree" to determine whether formula is satisfiable, it gives me wrong result:
Can you find my mistake and explain how is it done right?
Grant
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$.