Next: Generalized Subsumption Up: Selected Methods for Previous: Selected Methods for

Least General Generalization

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

  1. generalizes each clause in :
  2. is the smallest clause satisfying condition 1:

Harold Boley, Stefani Possner, Franz Schmalhofer (