Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?


share|cite|improve this question
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|cite|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
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


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.