Most-Specific-Generalization of Terms

The concept of most-specific-generalization (msg) was introduced independently by [Plotkin 70] and [Reynolds 70]. We focus on terms and atoms, rather than on wffs. 

Definition 10-1 Term 5 is less general than term t (denoted s t) iff there is a substitution o, such that 5 = ro. 

The relation /2 forms a complete lattice on the term set T (modulo variable renaming) to which a 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. 

Here follows another, constructive, definition of the concept of msg  

Definition 10-3 The most-specific-generalization of a non-empty set S of terms, denoted msg(S), is defined as follows  

---