(First order logic) Proof with resolution rule

Question

Hi I have following set of clauses:

$$\forall x \exists y (R(x,y))$$ $$\forall x \forall y (R(x,y) \to R(y,x))$$ $$\forall x \forall y \forall z ((R(x,y) \land R(x,z)) \to R(y,z))$$

I need to prove (using resolution rule) that: $$\forall x R(x,x)$$

I know already that it is provable by doing an informal proof. Since $\forall x \exists y (R(x,y))$ we can conclude that there is y for each x such that $R(x,y)$. By $\forall x \forall y (R(x,y) \to R(y,x))$ we see that there is also $R(y,x)$. Finally by $\forall x \forall y \forall z ((R(x,y) \land R(x,z)) \to R(y,z))$ we can conclude that $(R(y,x) \land R(y,x)) \to R(x,x)$ since $(x,y,z)$ can be arbitrarily chosen.

My question is how to transform above formulas by using resolution rule in order to get $\emptyset$. So by negating entire formula we recive following set of clauses that must by further handled:

Using skolemization on first one we get: $$R(x,f(x))$$ Second: $$\neg R(x,y) \lor R(y,x)$$ Third: $$\neg R(x,y) \lor \neg R(x,z) \lor R(y,z)$$ Finally we have negated conclusion ($a$ is constant): $$\neg R(a,a)$$

How to manipulate above clauses in order to prove entire formula and achieve $\emptyset$?

I'll appreciate any answer :)

Answer 1

We need Unification.

We have:

$R(x,f(x))$

$\lnot R(v,w) \lor R(w,v)$

$\lnot R(k,j) \lor \lnot R(k,h) \lor R(j,h)$

and the negation of the conclusion:

$\lnot R(a,a).$

First substitition: $a ↦ v$, $a ↦ j$, $a ↦ h$ and $k ↦ w$ to get:

$R(x,f(x))$

$\lnot R(a,k) \lor R(k,a)$

$\lnot R(k,a) \lor \lnot R(k,a) \lor R(a,a)$

$\lnot R(a,a).$

Applying the Resolution rule to 2nd and 3rd we get:

$R(x,f(x))$

$\lnot R(a,k) \lor R(a,a)$

$\lnot R(a,a).$

Now we need the substitution: $f(x) ↦ k$ and $a ↦ x$ to get:

$R(a,f(a))$

$\lnot R(a,f(a)) \lor R(a,a)$

$\lnot R(a,a).$

With resolution on 1st and 2nd:

$R(a,a)$

$\lnot R(a,a)$

and it is done.