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 [L1 ] for a brief overview and see Playing Prolog for basic implementation of a unification algorithm.
[ Category Concept ]