If $\neg A(x)\lor B(y),\neg C(x)\lor G(w),\neg G(x)$, and $A(x)$, then $B(x)\land \neg C(w)$

Use resolution and unification to do your proof. Justify each step.

I'm not sure how to correctly use Unification to get the correct variables where I want them. Here's what I tried:


$\neg A(x)\lor B(y)$

$\neg C(x)\lor G(w)$

$\neg G(x)$



$B(x)\land C(w)$


  1. $\neg B(x)\lor C(w)$ - Proof By Contradiction
  2. $\neg A(x)\lor B(y)$ - Premise
  3. $\neg A(x)\lor B(x)$ - Unification (Sub x in place of y) <--Can I do this?
  4. $C(w)\lor \neg A(x)$ - Resolution; Lines 1,3
  5. $\neg C(x)\lor G(w)$ - Premise
  6. $\neg C(w)\lor G(w)$ - Unification (sub w in place of x) <--OK?
  7. $\neg A(x)\lor G(w)$ - Resolution; Lines 4,6
  8. $\neg G(x)$ - Premise
  9. $\neg G(w)$ - Unification (sub w in place of x)
  10. $\neg A(x)$ - Resolution; Lines 7,9
  11. $A(x)$ - Premise
  12. FALSE - Resolution; Lines 10,11

So essentially, I substituted variables wherever I wanted whenever I need them. Is that how Unification(/Instantiation) works?

  • $\begingroup$ I don't understand why it's part of our curriculum. When a student asked why we were doing it, the prof gave a vague connection to programming... :/ To me, it was just an admission that there's no relevance $\endgroup$ – wad11656 Feb 17 '16 at 4:47
  • $\begingroup$ Resolution and unification are important in logic programming if you want to understand how the inference engine works. $\endgroup$ – Browning Feb 17 '16 at 18:47

You can use disjunctive syllogism to combine $\neg A(x)\lor B(y)$ with $A(x)$ to get $B(y)$.

Then combine $\neg C(x)\lor G(w)$ with $\neg G(x)$ to get $\neg C(x)$ the same way.

If you can then use unification to get the substitutions, you can finish up with an application of conjunction.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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