 First-order unification

First-order unification solves a finite system of equations between first-order terms. A useful rule presentation deletes $t=t$, orients $t=x$ to $x=t$ when $x$ is a variable, decomposes equal outer function symbols into argument equations, and rejects unequal outer function symbols. For $x=t$, reject a nontrivial occurrence of $x$ in $t$ by the occurs check; otherwise propagate the substitution $x\mapsto t$ through the other equations. A solved system assigns distinct variables that do not occur in its right sides.^[ref]

For example,first becomes $x=g(y),y=a$. Propagating $y\mapsto a$ gives $x=g(a),y=a$, hence a most general unifier. Keeping $x=g(y)$ without composing the later substitution would leave an unsolved dependency.

The rules preserve the possible unifiers, apart from explicitly rejecting impossible equations. Decomposition works because identical first-order terms have identical constructors and arguments. At a solved system, any other unifier is obtained by instantiating its remaining free variables; this proves the most general unifier property. Efficient implementations share term graphs rather than repeatedly copying growing first-order terms.