Artificial Intelligence
Prof R. Williams				


			    UNIFICATION


A key ingredient of the process of using the combination of modus ponens
and universal specialization to draw conclusions is determining what
to substitute for variables in order to make certain subexpressions
match.  For example, consider the two sentences:

1.  "Every person loves somebody."

2.  "John is a person."


We may translate these into predicate calculus as follows:

1.  (forall (x) (if (person x)
	            (exists (y) (and (person y) (loves x y)))))

2.  (person John)


Removing the quantifiers by the process of skolemization leads to:

1.  (if (person ?x) (and (person (sk-5 ?x)) (loves ?x (sk-5 ?x))))

2.  (person John)

The Skolem function sk-5 assigns to every person some person whom they love.

In order to apply modus ponens using sentences 1 and 2, we must find a
substitution for any variables involved so that the antecedent of
sentence 1 after this substitution has been performed on it matches
sentence 2 after the same substitution has been performed on it.
In this case it is clear that substituting John for ?x does the trick.
This process of specifying a substitution for variables that makes a set
of expressions identical to one another is called "unification."

In the example above, the two expressions that must be unified are

a1:	(person ?x)
a2:	(person John)

If we make the substitution John for ?x in both expressions, they become

a1':	(person John)
a2':	(person John)

which are identical.  We say that the substitution {?x/John} "unifies"
the two expressions a1 and a2, or that this substitution is a "unifier"
for these two expressions.

Another example:

b1:	(above ?z floor-19)
b2:	(above ?x ?y)

The substitution {?x/table-4, ?y/floor-19, ?z/table-4}
in this pair of expressions yields

b1':	(above table-4 floor-19)
b2':	(above table-4 floor-19)

Thus {?x/table-4, ?y/floor-19, ?z/table-4} is a unifier for b1 and b2.

But note that the substitution {?x/?z, ?y/floor-19} in b1 and b2 yields

b1'':	(above ?z floor-19)
b2'':	(above ?z floor-19)

so {?x/?z, ?y/floor-19} is also a unifier of b1 and b2.  We say that
{?x/?z, ?y/floor-19} is a more general unifier of b1 and b2 than
{?x/table-4, ?y/floor-19, ?z/table-4} because it has fewer variables
specialized (i.e., replaced by constants).  A "most general unifier" (MGU)
is one in which no variables are specialized which do not have to be.
The substitution {?x/?z, ?y/floor-19} is a MGU for b1 and b2.

The reason the MGU is important is that the result of all other substitutions
which unify the given set of expressions may be obtained by specializing from
the MGU substitution.

Some more examples:

c1:	(not (sees ?z ?y))
c2:	(not (sees ?z (feet-of ?z)))

{?y/(feet-of ?z)} is a MGU for c1 and c2.

d1:	(not (sees ?z ?z))
d2:	(not (sees ?z (feet-of ?z)))

These do not unify because there is no substitution which can make them
identical.

e1:	(and (is-a-member-of ?x ?y) (is-a-subset-of ?y ?z))
e2:	(and (is-a-member-of ?u ?v) (is-a-subset-of dog mammal))

{?x/?u, ?y/dog, ?z/mammal, ?v/dog} is a MGU for e1 and e2.