# Use unification and resolution to justify proof

Prove:

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:

Premises:

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

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

$\neg G(x)$

$A(x)$

Conclusion:

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

Proof:

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?

• 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 – wad11656 Feb 17 '16 at 4:47
• Resolution and unification are important in logic programming if you want to understand how the inference engine works. – 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.