Finding resolvent for clauses

Question

I have the following question and am not sure how to do it.

Find the resolvent for the clause $\lnot p(x) \lor p(f(a))$ with itself. How can I apply the resolution rule here?

Answer 1

To apply resolution of the clause with itself, first of all you make a copy of the clause in which you rename the $x$ variable.

$$ (\neg p(x) \vee p(f(a))) \wedge (\neg p(y) \vee p(f(a))) \enspace. $$

You then need to unify $p(y)$ and $p(f(a))$. The most general unifier in this case is obviously $\{y \leftarrow f(a)\}$. This gives you

$$ (\neg p(x) \vee p(f(a))) \wedge (\neg p(f(a)) \vee p(f(a))) \enspace. $$

Resolution gives you the original clause back.