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 :)


We need Unification.

We have:


$\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:


$\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:


$\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:


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

$\lnot R(a,a).$

With resolution on 1st and 2nd:


$\lnot R(a,a)$

and it is done.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.