Unification is used in [Logic programming] to find one or more instantiations
of the free variables in a set of logical formulas that satisfies those
formulas. See [http://en.wikipedia.org/wiki/Unification] for a brief overview and see
[Playing Prolog] for basic implementation of a unification algorithm.

----
[[ [Category Concept] ]]