unification 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:

A = p(f(u),v)

B = p(w,g(x))

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 I₁, where

I₁ = P(f(y), g(z))

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

I₂ = P(f(z),g(y))

I₃ = P(f(y),g(y))

I₄ = P(f(f(y)),g(g(z)))

I₅ = P(f(c),g(d))

Note that I₂, I₃, I₄, I₅ are themselves instances of I₁. In fact any common instance of A and B is an instance of I₁ and therefore I₁ 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 I₂. I₅ would also be one if c and d were variables rather than constants; indeed the y and z of I₁ could be any two distinct variables. In some cases A and B have no common instance; two examples of this are

A = P(f(u),v)

B = P(g(w),x)

and

A = P(f(u),u)

B = P(w,f(w))

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.

u·ni·fi·ca·tion / ˌyoōnəfiˈkāshən/ • n. the process of being united or made into a whole.DERIVATIVES: u·ni·fi·ca·tor·y / -ˈkātərē/ adj.