A first-order term is built from variables and fixed-arity constructors, for example

$$f(x,g(a))$$

where $x$ is a variable and $a$, $g$, $f$ are constructors or function symbols.

A substitution maps variables to terms. Applying

$$\theta={x\mapsto h(a),\ y\mapsto b}$$

to $f(x,y)$ produces $f(h(a),b)$.

Two terms unify when some substitution makes them syntactically equal. For example,

$$Pair(x,Int)$$

and

$$Pair(Bool,y)$$

unify with

$$x\mapsto Bool,\qquad y\mapsto Int.$$

Unification proceeds structurally: identical constructors require their corresponding arguments to unify; a variable can be bound to a term unless that would create an invalid self-reference. The occurs check rejects equations such as

$$x=f(x),$$

which have no finite first-order solution.

A most general unifier (MGU) makes only the substitutions forced by the equations. Any other unifier can then be obtained by further specializing the MGU.

First-order unification is a reusable algorithmic idea. Type inference uses it on type expressions; logic programming uses it to match queries with facts and rule heads; symbolic systems use related techniques to reconcile structured expressions.