A unifier of two terms or expressions is a substitution which makes them identical. A unifier 
is a most general unifier if every other unifier 
can be written as a composition 
for some substitution 
. When a most general unifier exists, it is unique up to
renaming of variables.
For example, the terms 
and 
have the most general unifier which
substitutes 
for 
and 
for 
.
Unifiers are used in automated theorem proving, term rewriting, and the operational
semantics of Prolog.
