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