Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question
up vote 2 down vote accepted

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.

share|cite|improve this answer
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. – Martin H. L. Feb 24 '13 at 18:36
Seems correct, yes. – Shaull Feb 24 '13 at 18:37

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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