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

- generalizes each clause in :
- is the smallest clause satisfying condition 1: