## 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 *I*_{1}, where *I*_{1} = *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*_{2} = *P*(*f*(*z*),*g*(*y*) *I*_{3} = *P*(*f*(*y*),*g*(*y*) *I*_{4} = *P*(*f*(*f*(*y*)),*g*(*g*(*z*))) *I*_{5} = *P*(*f*(*c*),*g*(*d*)) Note that *I*_{2}, *I*_{3}, *I*_{4}, *I*_{5} are themselves instances of *I*_{1}. In fact any common instance of *A* and *B* is an instance of *I*_{1} and therefore *I*_{1} 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*_{2}. *I*_{5} would also be one if *c* and *d* were variables rather than constants; indeed the *y* and *z* of *I*_{1} 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*)

*I*_{1} = *P*(*f*(*y*), *g*(*z*)

*I*_{2} = *P*(*f*(*z*),*g*(*y*)

*I*_{3} = *P*(*f*(*y*),*g*(*y*)

*I*_{4} = *P*(*f*(*f*(*y*)),*g*(*g*(*z*)))

*I*_{5} = *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*))

**From:**
unification
in
A Dictionary of Computing »

*Subjects:*
Computing.

## Related content in Oxford Index

##### Reference entries

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