# first order logic resolution unification

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


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.
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.