Predicate Calculus - Resolution

Question

A question came up at the our schools logic club this week which involves using resolution to prove an argument in predicate calculus. I am slightly aware of how to find prenex normal forms but to actually solve the question I am having some difficulty. The question is as follows:

Use resolution for predicate calculus to prove that the argument below is valid. (find the prenex normal forms of the required formulas, then the ∃-free prenex normal forms, transform them into clauses and perform resolution). Describe in details all your work.

Premise 1: ∃x(P(x) ∧ ¬Q(x, a))
Premise 2: ∃x[P(x) ∧ ∀y(P(y) ∧ R(x, y) → Q(y, a))]
Conclusion: ∃x∃y(P(x) ∧ P(y) ∧ ¬R(x, y))

Thanks for the help.

Answer 1

Hint

The prenex normal forms are trivial; thus we can go directly to the "elimination" of $\exists$.

From Premise 1 we get :

$P(b) \land \lnot Q(b,a)$

and from Premise 2 we get :

$P(c) \land [\lnot P(y) \lor \lnot R(c,y) \lor Q(y,a)]$.

Thus, we have 4 clauses :

1) $P(b)$

2) $\lnot Q(b,a)$

3) $P(c)$

4) $\lnot P(y) \lor \lnot R(c,y) \lor Q(y,a)$.

Then we add the negation of the Conclusion, which is again a clause :

6) $\lnot P(x) \lor \lnot P(y) \lor R(x, y)$.

Now we have to perform Resolution, starting from 1) and 3) with the unifiers :

$b \to y$ and $c \to x$.