Unification is the process of solving equations in term algebra, which is the algebra of ground terms, with functions defined as in the Ground Terms section of proof of Herbrand theorem.

The solution process is essentially variable elimination, based on two main properties

  • equation $f(t_1,\ldots,t_n) \doteq f(s_1,\ldots,s_n)$
  • equation $f(t_1,\ldots,t_n) \doteq g(s_1,\ldots,s_m)$ where $f \neq g$
  • equation $x \doteq t(x)$ where $t$ is a term containing $x$ but not identical to $x$


First-order language:

  • $R$ - binary relation symbol
  • $f$ - binary function symbol
  • $a,b,c$ - constants
  • $x,y,z,u,v,w$ - variables

Example 1

  R(x,f(x,y)) \doteq R(f(a,v),f(f(u,b),f(u,u)))

Example 2

  R(x,f(x,x)) \doteq R(f(a,v),f(f(u,b),f(u,u)))

Example 3

  R(x,f(x,y)) \doteq R(f(u,v),v)

Definition: Unifier of a set $E$ of syntactic equations is a substitution that makes all equations true.

Definition: Composition $\circ$ of substitutions.

Definition: A renaming is a substitution which is (a total function and) a bijection on the set of all variables.

Lemma: If $\sigma$ is a unifier for $E$ and $\tau$ is a substitution, then $\tau \circ \sigma$ is also a unifier.

A unifier is a solution of equations. mgu is the most general solution.

Definition: A most general unifier for $E$ is a unifier $\sigma$ such that if $\sigma'$ is another unifier, then there exists a substitution $\tau$ such that $\sigma' = \tau \circ \sigma$.


We next sketch an algorithm for computing mgu.

A set of equations is in solved form if it is of the form $\{ x_1 \doteq t_1,\ldots, x_n \doteq t_n \}$ iff variables $x_i$ do not appear in terms $t_j$, that is

   \{x_1,\ldots,x_n \} \cap (FV(t_1) \cup \ldots FV(t_n)) = \emptyset

We obtain a solved form in finite time using the non-deterministic algorithm that applies the following rules as long as no clash is reported and as long as the equations are not in solved form.


Select $t \doteq x$ where t is not x, and replace it with $x \doteq t$.


Select $x \doteq x$, remove it.


Given $x \doteq t$ where $x$ does not occur in $t$, substitute $x$ with $t$ in all remaining equations.

Occurs Check

Given $x \doteq t$ where $x$ occurs in $t$, report clash.


Given $f(t_1,\ldots,t_n) \doteq f(s_1,\ldots,s_n)$, replace it with $t_1 \doteq s_1,\ldots,t_n \doteq s_n$.

Decomposition Clash

Given $f(t_1,\ldots,t_n) \doteq g(s_1,\ldots,s_m)$ for $f$ not $g$, report clash