Unifier

A unifier of first-order terms $s,t$ is a first-order substitution $\sigma$ for which $s\sigma =t\sigma$. The first-order substitution replaces variables by first-order terms; it does not alter function symbols. For example, $\{x\mapsto a,y\mapsto b\}$ unifies $f(x,g(y))$ with $f(a,g(b))$.

A most general unifier leaves every identification not forced by the original equations available for later choice. For $f(x,y)=f(y,z)$, one solution is $\{x\mapsto z,y\mapsto z\}$. The remaining variable $z$ is free. Replacing it by any finite first-order term gives a more specific unifier; arbitrarily choosing $z=a$ during the initial computation would discard that generality.

Not every pair is unifiable. Distinct constant symbols cannot be made equal by replacing variables, and the occurs check rejects $x=f(x)$ for finite first-order terms. These are structural restrictions, not numerical inequalities. Unifiers allow a resolution step to align the relevant atomic formulas before the logical inference is performed.^[ref]