Anti-unification

The relation least element has been added [Lassez et al. 87]. The gib operator computes the gci (greatest common instance) of two terms (by a unification algorithm). The lub operator computes the msg of two terms (by an anti-unification algorithm). The msg of two terms thus always exists, and is unique up to variable renaming. 

As said earlier, the concepts of msg and anti-unification were introduced simultaneously, but independently, by [Plotkin 70, 71] and [Reynolds 70]. The original motivation is accredited to [Popplestone 70], who suggested that since unification is useful in automatic deduction by the resolution method, its dual might prove helpful for induction . The main differences between both works are that Plotkin takes a logic-based approach and considers atomic formulas and clauses, whereas Reynolds is more concerned about an algebraic approach and only considers atomic formulas. But their results and msg algorithms are essentially the same. 

---