Overview

unification


Show Summary Details

Quick Reference

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 I1, where I1 = 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 I2 = P(f(z),g(y) I3 = P(f(y),g(y) I4 = P(f(f(y)),g(g(z))) I5 = P(f(c),g(d)) 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 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.

A = p(f(u),v)

B = p(w,g(x)

I1 = P(f(y), g(z)

I2 = P(f(z),g(y)

I3 = P(f(y),g(y)

I4 = P(f(f(y)),g(g(z)))

I5 = P(f(c),g(d))

A = P(f(u),v)

B = P(g(w),x)

A = P(f(u),u)

B = P(w,f(w))

Subjects: Computing.


Reference entries

Users without a subscription are not able to see the full content. Please, subscribe or login to access all content.