
Chapter
15:
Unification
Revisited
589
In "Most General Unifiers," we establish the relationships between mgus,
idempotent mgus, and reduced sets of equations, formally clarifying the
dif-
ferences between the definitions of Herbrand, Robinson, and Chang and Lee.
In "Anti-unification and Most General Solutions," we show the existence
of a most general solution (mgs) to a set of equations by using anti-unification.
We also investigate the relationship between mgs and equations in solved form.
As an application of the anti-unification algorithm, we give an algorithm to
compute the most specific generalization of a collection of sets of equations ...