Definition
Most General Unifier
A most general unifier of two expressions
and is a unifier such that every other unifier factors through . Formally,
is a most general unifier iff: and for every unifier
with , there exists a substitution such that Thus
makes and equal while committing to no unnecessary substitutions.