Find the resolvent of the following clause

Question

Find the resolvent of the following clause with itself

$p(x) \lor \lnot p(f(a)) \lor q(x)$

Can someone verify if im doing this correct?

Step 1: rename variables

$p(x) \lor \lnot p(f(a)) \lor q(x) \land p(y) \lor \lnot p(f(a)) \lor q(y) $

Step 2: find most general unifier

replace y with f(a)

$p(x) \lor \lnot p(f(a)) \lor q(x) \land p(f(a)) \lor \lnot p(f(a)) \lor q(f(a)) $

step 3:

by resolution rule

$p(x) \lor \lnot p(f(a)) \lor q(x) \lor q(f(a)) $

and why isn't $p(f(a))$ included in the solution? is it because it's the same as $p(x)$ ?

Answer 1

Yes, that's correct.

$p(f(a))$ is not included since you resolved on that, removing $p(f(a))$ from the second clause, and $\neg p(f(a))$ from the first. If you are wondering why there still is a $\neg p(f(a))$ it's because that one was in the second clause as well.

For future efforts, it may be helpful to more clearly separate the clauses. That is, you have:

Clause 1: $p(x) \lor \neg p(f(a)) \lor q(x)$

Clause 2: $p(y) \lor \neg p(f(a)) \lor q(y)$

That way, the $\land$ isn't distracting you.

Answer 2

I actually wanted to add a comment, but I cannot due to being new here, so I am forced to write it as an answer..

First of all it would be nice to get a source of your course or a book with which you are working, because Resolution is usually defined for literals and not what you present here. So it would be nice to see the context from where you arrive at your question.

I assume that $x$ and $y$ are variables and $f(a)$ is a term in some constant $a$, but this is nowhere specified. Then you just substitute $f(a)$ for $y$, which I find rather questionable. This means that you arbitrarily assign a truth value to a propositional formula and in your case, you actually produce $p$ and $\neg p$ in the same clause, i.e. you set that clause to $true$.

On a side note, please use brackets. Usually one would say that $\wedge$ binds stronger than $\vee$ and that is not what you want.