Unification [18] is a pattern-matching technique used in automated theorem proving, type-inference systems, computer algebra, and logic programming, e.g., Prolog [3].

A unification algorithm attempts to make two symbolic expressions equal by computing a unifying substitution for the expressions. A substitution is a function that replaces variables with other expressions. A substitution must treat all occurrences of a variable the same way, e.g., if it replaces one occurrence of the variable x by a, it must replace all occurrences of x by a. A unifying substitution, or unifier, for two expressions e1 and e2 is a substitution, σ, such that σ(e1) = σ(e2).