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)
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.
"unification." A Dictionary of Computing. . Encyclopedia.com. (January 18, 2019). https://www.encyclopedia.com/computing/dictionaries-thesauruses-pictures-and-press-releases/unification
"unification." A Dictionary of Computing. . Retrieved January 18, 2019 from Encyclopedia.com: https://www.encyclopedia.com/computing/dictionaries-thesauruses-pictures-and-press-releases/unification
Encyclopedia.com gives you the ability to cite reference entries and articles according to common styles from the Modern Language Association (MLA), The Chicago Manual of Style, and the American Psychological Association (APA).
Within the “Cite this article” tool, pick a style to see how all available information looks when formatted according to that style. Then, copy and paste the text into your bibliography or works cited list.
Because each style has its own formatting nuances that evolve over time and not all information is available for every reference entry or article, Encyclopedia.com cannot guarantee each citation it generates. Therefore, it’s best to use Encyclopedia.com citations as a starting point before checking the style against your school or publication’s requirements and the most-recent information available at these sites:
Modern Language Association
The Chicago Manual of Style
American Psychological Association
- Most online reference entries and articles do not have page numbers. Therefore, that information is unavailable for most Encyclopedia.com content. However, the date of retrieval is often important. Refer to each style’s convention regarding the best way to format page numbers and retrieval dates.
- In addition to the MLA, Chicago, and APA styles, your school, university, publication, or institution may have its own requirements for citations. Therefore, be sure to refer to those guidelines when editing your bibliography or works cited list.
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.
"unification." The Oxford Pocket Dictionary of Current English. . Encyclopedia.com. (January 18, 2019). https://www.encyclopedia.com/humanities/dictionaries-thesauruses-pictures-and-press-releases/unification
"unification." The Oxford Pocket Dictionary of Current English. . Retrieved January 18, 2019 from Encyclopedia.com: https://www.encyclopedia.com/humanities/dictionaries-thesauruses-pictures-and-press-releases/unification