Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

share|improve this question

1 Answer 1

up vote 1 down vote accepted

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$.

share|improve this answer
    
Thank you! I thought that I can cross out more than one proposition at time. –  Grant Dec 30 '12 at 18:32
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. –  MJD Dec 30 '12 at 18:34

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.