I was given the following 2 sentences:
1) ∀x (Boy(x) => ∃y (Girl(y) ∧ Likes(x,y)))
2) ∃y (Girl(y) ∧ ∀x (Boy(x) => Likes(x,y)))
Then I was asked to prove, with resolution, that sentence 1 follows from sentence 2.
To do this I first negated the first sentence and then converted the negated first sentence and the second sentence to conjunctive normal form. These are my results:
A) ¬Girl(W) ∨ ¬Boy(v) ∨ Likes(v,W)
B) Boy(X)
C) ¬Girl(y) ∨ ¬Likes(X,y)
However, it doesn't seem possible to come to a contradiction (an empty resolvent) with these 3 clauses. There will always be a ¬Girl(W) left. I cannot figure out what I'm doing wrong. Are my sentences in CNF wrong or can you come to a contradiction with the 3 sentences (A, B and C) given above?
The negation of $\forall x~(B(x)\to \exists y~(G(y)\wedge L(x,y)))$ is $~\exists x~\forall y~(B(x)\wedge (\neg G(y)\vee \neg L(x,y)))~\color{green}{\checkmark}$
But the CNF of $\exists y~(G(y)\wedge \forall x~(B(x)\to L(x,y)))$ is $~~\exists y~\forall x~(G(y)\wedge(\neg B(x)\vee L(x,y)))$
And remember, existences are bound values, universals are unbound. So you must resolve: $$B(b)~,~\neg G(Y)\vee\neg L(b,Y)~,~ G(a)~,~\neg B(X)\vee L(X,a)$$