An operation on well-formed formulas, namely that of finding a most general common instance. The formulas can be terms or atomic formulas (see predicate calculus). A common instance of two formulas A and B is a formula that is an instance of both of them, i.e. that can be obtained from either by some consistent substitution of terms for variables. As an example let A and B be the following:
Let
u, v, w, x, y, z be variables, and
c, d constants. Consider the substitution that replaces
u, v, w, x respectively by the terms
y, g(
z),
f(
y),
z. This substitution, when applied to
A and
B, transforms them both into the same formula
I1, where
Hence the above is a common instance of
A and
B. It is however only one of infinitely many: other common instances of
A and
B include
Note that
I2,
I3,
I4,
I5 are themselves instances of
I1. In fact any common instance of
A and
B is an instance of
I1 and therefore
I1 is called a
most general common instance of
A and
B. Of the formulas above, the only other one that is a most general common instance is
I2.
I5 would also be one if
c and
d were variables rather than constants; indeed the
y and
z of
I1 could be any two distinct variables. In some cases
A and
B have no common instance; two examples of this are
and
If
A and
B do have a common instance however, they must have a most general one. There are algorithms (the original one being Robinson’s, 1965) for deciding whether a given
A and
B have a common instance, and if so finding a most general one. Robinson’s motivation for describing unification was its role in resolution theorem proving. Resolution was at one time associated with ‘general problem-solving’ techniques in artificial intelligence. More recently it has provided the conceptual basis for the logic programming language Prolog. Another use of unification is in compile-time type-inference, especially for polymorphic types.