first order logic resolution unification

Question

Assuming I have shown part of the knowledge base in the clausal format:

[1] p1(banana).

[2] not p1(X) or p2(Y).
[3] p1(X) or not p3(F).

... and more rules.

Most of the books, would do something like this:

[1,2] {X=banana} p2(Y).

and more steps.

First question: is it equally correct to do something like follows:

[2,3] {X=X} p2(Y) or not p3(F).

and then continue with resolution.

Second question: What if different variables were used in each clause, could I do the same as above, for example we had:

[2] not p1(X1) or p2(Y1).
[3] p1(X2) or not p3(F2).

[2,3] {X1=X2} p2(Y) or not p3(F2).

Thank you in advance

Answer 1

Assuming $X$ here is a variable, rather than an atomic proposition, then first you must specify what is the quantification for 2 and 3. I assume that it should be

$\forall X,Y \neg p1(X)\vee p2(Y)$, and similarly for 3. In this case, what can be done is to replace $X$ and $Y$ with each atomic proposition available, in order to obtain a propositional knowledge base, and work on that.

What you suggest to do with 2,3 is sound only under universal quantification, but if you have only universal quantification, it is useful indeed.

For your second question: the name of the variable means nothing, so your substitution is sound also there. Indeed, the claim $\forall Y, P(Y)$ is equivalent to $\forall Z, P(Z)$. You can first change the names, if it makes you happy :)

I'll remark that usually, in resolution-guided proofs, it is more useful to resolve a concrete expression with a quantified rule. For example, resolving $P(a)$ with $\forall X P(X)\to Q(X)$ in order to obtain $Q(a)$. This is more likely (heuristically) to get you towards the proof of a claim.