Unification is the process of determining 
whether two expressions can be unified, 
that is made identical, by appropriate 
substitutions for the variables. 
As we'll see shortly, making this 
determination is an essential part of 
resolution. 
A substitution is a finite mapping of 
variables to terms. 
What follows will right substitution as 
sets of replacement rules like the one 
shown here. 
In each rule the variable to which the 
arrow is pointing is to be replaced by 
the term from which the arrow is 
pointing. 
In this case, x is to be replaced by a, y 
is to be replaced by f of b and v is to 
be replaced by w. 
The result of applying a substitution, is 
called sigma, to an expression phi is the 
expression written phi sigma. 
Obtained from phi by replacing every 
occurrence of every variable in sigma. 
By the term with which it is associated. 
For example applying our substitution to 
the expression p of x, x y z, yields p of 
a, a f of b and z. 
Given two or more substitutions, it's 
possible to define a single substitution 
that has the same effect as applying 
those substitutions in sequence. 
For example, the substitutions x gets a, 
y gets f of u, z gets v. 
And, u gets d, v gets e and z gets g, can 
be combined to form the single 
substitution, x gets a, y gets f of d, z 
gets e, u gets d and v gets e. 
And the single substitution has the same 
effect as the first two substitutions 
when applied to any expression 
whatsoever. 
Computing the composition of a 
substitution sigma, the cup substitution 
toa is easy. 
Okay, there are three steps. 
First we take too and apply it to the 
replacement in sigma. 
Having done that, we join to sigma 
or[UNKNOWN] which are different variables 
than those in sigma. 
Notice that in this case we did not 
inlcude the binding of z to g from toa 
because we already had a binding of z to 
e in sigma. 
Finally in the third step we delete any 
assignments of variables to themselves. 
No examples of that in this case. 
Okay now why do we care about 
substitutions? 
Well it's the first step in unification. 
Say a substitution sigma is a unifier for 
an expression phi and expression psi. 
If and only if phi sigma is the same as 
psi sigma. 
Now, does sigma apply to psi, does sigma 
psi apply to psi, produce the same 
expression? 
If two expressions have a unifier, 
they're said to be unifiable. 
And otherwise they're nonunifiable. 
So an example of nonunifiable expressions 
is shown here. 
would be p of x,x on the one hand and p 
of a,b on the other. 
There's no way to bind x so that, it's 
the same as a and at the same time the 
same as b. 
Okay now, although the substitution 
unifies two expressions, it may not be 
the only unifier. 
We don't have to substitute b for y and v 
to unify two expressions. 
We can equally well substitute c, or d, 
or f of c, or f of w. 
In fact, you can unify these expressions 
without changing v at all by simply 
replacing y by v. 
Now in considering these alternatives it 
should be clear that some substitutions 
are more general than others. 
In fact we're going to enshrine that with 
a definition. 
We say that a substition sigma is as 
general as, or more general than, a 
substititon tao. 
If and only if there's another 
substitution delta such that tao is the 
composition of sigma and delta. 
For example, the substitution at the 
bottom here is more general, as are more 
general than the other two, since each 
can, of the first two can be contained by 
composing unifier at the bottom with 
another substitution. 
And in fact, the substitution at the 
bottom is more general than the other two 
in that the reverse does not hold. 
There's no way to convert either one of 
the first two into the third unifier by 
applying an additional substitution. 
Now, in resolution we're interested only 
in unifiers with maximum generality. 
It's called a most general unifier, or 
mgu, and it's defined as follows. 
An mgu sigma of two expressions has the 
property that is as general as or more 
general than any other unifier. 
Now, it's possible for two expressions to 
have more than one most general unifier. 
However, even this, as though this is the 
case, all of the most general unifiers 
are structurally the same. 
And, in otherwords, they're unique up to 
variable renaming. 
For example, p of x and p of y can be 
unified by either the substitution x gets 
y or by the substitution y gets x. 
And either of these substitutions can be 
obtained from the other by applying a 
third substitution. 
It's not true of those unifiers we saw 
earlier. 
Okay, one good thing about our language 
is that there is a simple and quite 
inexpensive procedure for computing the 
most general unifier of any two 
expressions provided that there is one. 
the procedure assumes a representation of 
expressions as sequences of 
subexpressions. 
For example, the expression p of a, f of 
b and z can be thought of as a sequence 
with four elements, namely the relation 
constant p, the object constant a, the 
term f of b. 
I'm sorry f of b, c. 
And the variable z. 
The term f of b, c can in turn be thought 
of as sequence of three elements namely 
the function constant f, the object 
constant b and the object constant c. 
Okay, given that representation, we can 
describe the procedure. 
in detail. 
You start with two express, 
subexpressions, and a sub, and an empty, 
a substitution, which is initially empty. 
We then recursively process the two 
expressions, comparing the subexpressions 
of the, those expressions at each point. 
Along the way, we expand the substitution 
with variable assignments, as we'll see. 
If we fail to unify any pair of 
subexpressions at any point in the 
process the procedure as a whole fails. 
If we finish the recursive comparison of 
the expressions, the procedure as whole 
succeeds, and the accumulated 
substitution at that point is our most 
generally unifier. 
Okay the rules are these. 
If two expressions being compared into 
sub expressions being compared are 
identical, we succeed on that step. 
If neither one is a variable and at least 
one is a constant, then we fail. 
If at least one of the expressions is a 
variable, we proceed as described in just 
a moment. 
However, both expressions are sequences, 
neither variables nor constants, then we 
iterate across the expressions, comparing 
sub-expression to sub-expression, as just 
described, in the same manners just 
described. 
Okay, now what about the case where we 
have at least one of the expressions 
being a variable? 
Alright, in this case we first check 
whether the variable has a binding in the 
current substitution. 
If so, we try to unify that binding with 
the other expression. 
If there's no binding, we can give it a 
binding, but first we check whether the 
second expression contains the variable 
that, to which we are binding it. 
That the variable occurs within the 
expression, we fail. 
Otherwise we set the substitution to com, 
the composition of the old substitution 
and a new substitution which we bind the 
variable to that second expression. 
This will all become a lot clearer when 
you look through some examples, right 
now. 
So here's our first example. 
Instead of the computation of the most 
general unifier for the expressions p of 
xb and p of ay, with the initial 
substitution empty. 
The trace of the execution or procedure 
for this case is shown here. 
we show the beginning of a comparison, 
with a line labeled, call. 
Together with the expressions being 
compared, and the input substitution. 
And we show the result of that comparison 
with the line label x. 
At each point here, the indentation shows 
the depth of incursion of the procedure. 
Okay, so here on the first[UNKNOWN] step, 
we compare the first element of the first 
expression with the first element of the 
second expression, since they're 
identical in this case, we succeed with 
no changes to our substitution. 
We then compare the variable x to the 
constant a, in this case, leading to a 
binding of x to a. 
And finally we compare b to y. 
In this case we compose the current 
variable assigment x gets a with the 
assignment y to b which produces the 
joint assignment x gets a y gets b. 
At this point having reached the ends of 
both expressions, we're done. 
Okay here's another example, consider 
unifying the expressions p of x, x and 
the expression p of a, y. 
Here's our trace, main interest in this 
case is in the step involving x and y. 
So at this point x has a binding to a, 
and so we recursively compare that 
binding of y replacement, which is a in 
this case, to y. 
In this case, we can bind y to a, we 
could pose that substitution with the 
original substitution to reduce the 
resulting a composite substitution, x 
gets a and y gets a. 
And again since we're done processing all 
the sub expressions the substitution at 
this point is the most generally unifier. 
Okay, using example where two expressions 
do not unify. 
Start same as before. 
This time when we compare the second x to 
b, get a different result. 
As before we retrieve that binding of x 
namely a and try to unify a with b. 
Since its two different constants we fail 
and unification as a whole fails. 
Okay here's one more example. 
This one's similar to that last one 
except that the second term in the second 
expression is the functional term that 
contains y. 
After unifying the first two arguments, 
we find ourselves trying to unify. 
x and f of y. 
With a substitution where x is bound to 
y. 
Now in order for this to work we would 
have to unify y and f of y. 
We would have to bind y to f of y. 
But now remember back to the condition 
that I mentioned on variable assignments. 
We must not ever bind a variable to a 
term which contains itself. 
Since f of y contains y, the 
substitution, unification process in this 
case fails, and the unification process 
as a whole fails. 
Okay now you might be wondering why 
exactly we have this condition, that a 
variable may not be bound to itself. 
Okay well one reason is this, if we were 
to allow bindings of variables to 
expressions that contain those variables, 
it would lead to circular bindings. 
Now this in itself is not a problem, 
though it does raise the question, how 
many times the substitution needs to be 
applied. 
more importantly though, it can create a 
situation where the substitution does not 
actually unify the input expressions, no 
matter how many times it's applied. 
Okay, as we see here, applying a 
substitution does not lead to the same 
result. 
And, it fails no matter how many more 
times we apply it. 
The second argument in the second case 
always has one additional applicational 
f. 
And so these expressions will never look 
alike. 
it's the reason why we check, whether 
variables contained in an expression 
before creating a binding, and it has a 
name, it's so important this condition. 
It's called the occur check for obvious 
reasons. 
interestingly though, not all logical 
systems do this occur check. 
Prolog, the programming language Prolog, 
is notable for not performing the occur 
check, or at least not by default in most 
systems. 
programatically it's useful as a way of 
generating circular data structure, or 
logically it can lead to errors and so in 
logic we always do the occur checking 
resolution.