Predicate Calculus - Resolution 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.

**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$.