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


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

  • $\begingroup$ Thanks for the reply. X,Y,F, X1, Y1, F2, Y2 all represent variables. Yes they should be universally quantified, otherwise during converting to clauasal format, they should be replaced by constants or functions. So in that case, is my approach correct? This was my impression. $\endgroup$ Feb 24, 2013 at 18:36
  • $\begingroup$ Seems correct, yes. $\endgroup$
    – Shaull
    Feb 24, 2013 at 18:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.