In mathematical logic, in particular as applied to computer science, a **unification** of two terms is a *join* (in the lattice sense) with respect to a **specialisation order**. That is, we suppose a preorder on a set of terms, for which *t** ≤ *t* means that *t** is obtained from *t* by substituting some term(s) for one or more free variables in *t*. The unification *u* of *s* and *t*, if it exists, is a term that is a **substitution instance** of both *s* and *t*; and such that any common substitution instance of *s* and *t* is also an instance of *u*.

For example, with polynomials, *X*^{2} and *Y*^{3} can be unified to *Z*^{6} by taking *X* = *Z*^{3} and *Y* = *Z*^{2}.

The concept of **unification** is one of the main ideas behind Prolog. It represents the mechanism of binding the contents of variables and can be viewed as a kind of one-time assignment. In Prolog, this operation is denoted by symbol "=".

- An uninstantiated variable
*X*(i.e. no previous unification were performed on it) can be unified with an uninstantiated variable (and effectively becomes its alias), an atom or a term. - An atom can be unified only with the same atom.
- A term is unified with another term, if the heads and arities of the terms are identic and the parameters are unified (note that this is a recursive behaviour).

; *A*=*A* : Succeeds (tautology)
; *A*=*B*, *B*=abc : Both *A* and *B* are unified with the atom abc
; xyz=*C*, *C*=*D* : Unification is symmetric
; abc=abc : Unification succeeds
; abc=xyz : Fails to unify, atoms are different
; f(*A*)=f(*B*) : *A* is unified with *B*
; f(*A*)=g(*B*) : Fails, the heads of terms are different
; f(*A*)=f(*B*,*C*) : Fails to unify, because terms have different arity
; f(g(*A*))=f(*B*) : Unifies *B* with the term g(*A*)
; f(g(*A*), *A*)=f(*B*, xyz) : Unifies *A* with the atom xyz and *B* with the term g(xyz)
; *A*=f(*A*) : Infinite unification, *A* is unified with f(f(f(f(...)))).
; *A*=abc, xyz=*X*, *A*=*X* : Fails to unify; effectively abc=xyz