Resolution in FOL? Renaming and substituting variables?

Question

I would just like to know if this is the correct way to do resolution in FOL.

Original Clauses:

1. ¬p(x,y) ∨ p(y,x)

2. ¬p(x,y) ∨ ¬p(y,z) ∨ p(x,z)

3. p(x,f(x))

4. ¬p(x,x)

Renaming variables:

1. [x/x1], [y/y1]
2. [x/x2], [y/y2]
3. [x/x3],
4. [x/x4]

Renamed clauses:

1. ¬p(x1,y1) ∨ p(y1,x1)

2. ¬p(x2,y2) ∨ ¬p(y2,z) ∨ p(x2,z)

3. p(x3,f(x3))

4. ¬p(x4,x4)

New/resolvent clauses:

5. Substitutions: Clause1 - [y1/f(x1)], Clause 3 - [ x3/ x1].

   Resolvent Clause from clause1 & clause 3: p(f(x1), x1)

6. Substitutions: Clause2 - [y2/f(x1)], [z /x1], Clause 3 - [ x3/ x1].

   Resolvent Clause from clause2 & clause 5: ¬p(x2,f(x1) ∨ ¬p(x2,x1)

7. Substitutions: Clause6 - [ x2/ x4],[ x1/ x4].

   Resolvent Clause from clause4 & clause 6: ¬p(x4,f(x4))

8. Substitutions: Clause7 - [ x4/ x3]

   Resolvent Clause from clause3 & clause 7:[]

So, I would like to know if my approach is correct? Also, I will like to know when I could not make a substitution? Are these the only kind of substitutions I can't make, [x/x] and [x/f(x)]?

Any help will be much appreciated! Thanks!

Answer 1

Hint

Maybe try with a "smart" approach, prior to any renaming:

• subst $x \to z$ in 1) and 2) to get:

5) $¬p(x,y) ∨ p(x,x)$

• resolve with 4) to get:

6) $¬p(x,y)$.

Now we have :

3) $p(x,f(x))$

6) $¬p(x,y)$.

Now we can unify with subst: $f(x) \to y$.

---

Also with your initial renaming, I'll try with:

• subst $x_4 \to z$ and $x_4 \to x_2$ in 2) to get:

2') $¬p(x_4,y_2) ∨ ¬p(y_2,x_4) ∨ p(x_4,x_4)$

and resolve with 4) to get:

5) $¬p(x_4,y_2) ∨ ¬p(y_2,x_4)$.

Then subst $x_4 \to x_1$ and $y_2 \to y_1$ in 1) to get:

1') $¬p(x_4,y_2) ∨ p(y_2,x_4)$

and resolve with 5) to get:

6) $¬p(x_4,y_2)$.

Now we have:

3) $p(x_3,f(x_3))$

6) $¬p(x_4,y_2)$

and we can define the final subst to resolve them.