Least general generalization was originally introduced by Plotkin [\protect\citeauthoryearPlotkin1970]. It is the opposite of most general unification [\protect\citeauthoryearRobinson1965]; therefore it is also called anti-unification. Given two atomic formulas and , unification computes their most general specialization while anti-unification computes their most special generalization .
In addition to the generalization of literals, Plotkin also describes an algorithm for the least generalization of clauses. A clause generalizes a clause (denoted by ), if subsumes , i.e. there exists a substitution such that . This is also called -subsumption [\protect\citeauthoryearBuntine1988]. A generalization of a clause can thus be obtained by applying a -subsumption-based generalization operator that maps a clause to a set of clauses which are generalizations of . Informally speaking, if clause -subsumes clause , then can be converted to by (1) dropping premises and (2) turning constants to variables. A clause is a least generalization of a set of clauses S, if