Variables and Resolution

Standardizing Variables Apart While Converting to Clauses

The following are equivalent:
Resolution seeks ways in which particular variable bindings can satisfy a formula (a disjunction of literals, a clause, that is), given a more complex formula (a conjunction of disjunctions of literals, two clauses, that is). Given any of the above (each of which constitutes two clauses), for example, we can infer the following single clause:

That is, For all x and y, if x is y's father, then x can't be y's mother.
But this doesn't allow us to find the contradiction in the following set of clauses:

(Note that we could find the contradiction if we resolved in a different order.) But what we really want is the most general substitution that makes the relationship between Mother and Father true. The following is also true, given any of 1-4 above:

That is, for all x and y and b, if x is y's father, then x can't be b's (i.e., anybody's) mother. Note that inference (6) is less restrictive than (5).
In order to ensure that we find the most general substitution, we standardize variables apart when changing to clause form. That is, we make each clause have a unique set of variables. So (4) above is the version of (1) which we work with. In standard clause notation:
Now we proceed as follows, given (6) and (7) as well as (9) and (10).
Resolving (9) and (10)
Resolving (11) and (6)
Resolving (12) and (7)

Standardizing Variables Apart Following Resolution

If x is above y, and y is above z, then x is above z. A is above B, B is above C, and C is above D. Is A above D?

In clause form (Scheme format):

((~ (above ?x ?y))  (~ (above ?y ?z))  (above ?x ?z))   (1)
(above A B)                                             (2)
(above B C)                                             (3)
(above C D)                                             (4)
(~ (above A D))                                         (5)

Resolving (5) with (1) gives the following (without standardizing variables apart)

((~ (above A ?y)  (~ (above ?y D)))                     (6)

Resolving (6) with (1) (substitution x=A and z=y) gives
```
((~ (above A ?y))  (~ (above ?y ?y))  (~ (above ?y D))) (7)
```
But this is too restrictive; it seems to require something that is between A and D which is above itself.

Standardizing variables apart, (6) becomes instead

((~ (above A ?w)  (~ (above ?w D)))                     (8)

Resolving (8) with (1) (substitution x=A and w=z) gives
```
((~ (above A ?y))  (~ (above ?y ?z))  (~ (above ?z D))) (9)
```
This says that there should be something which is below A and above something which is above D in order to find the contradiction. Successive resolution of (9) with (2), (3), and (4) yields the empty clause.
Thus each time a clause results from resolution, it should be assigned unique variables.

Representation and Reasoning: Conversion to Clause Form

Representation and Reasoning: Resolution Theorem Proving as Search

Last updated: 13 February 1996
URL: http://www.indiana.edu/~gasser/Q351/variables.html
Comments: gasser@salsa.indiana.edu
Copyright 1996, The Trustees of Indiana University