Catalogue of Artificial Intelligence Techniques
Least General Generalisation
Keywords: least general generalisation
Categories: Theorem Proving , Inference and Reasoning , Logic Programming
Author(s): Steve Muggleton
Plotkin showed that there exists a dual of the most general unifier of two literals. Suppose that the most general unifying substitution (see Unification) for two first-order literals, and is . Then
is called the most general instance (mgi) of
and . Like the most general instance, the least general generalisation (lgg) of and does not always exist. However, whenever and have the same predicate symbol and sign their lgg is unique up to renaming of variables. Generalisation over literals is defined by subsumption. subsumes
whenever there exists a substitution such that
. Plotkin showed that due to the uniqueness of the least general generalisation and most general instance, subsumption forms a infinite semi-lattice over first-order literals. Plotkin extends this result to show that the same holds for subsumption over clauses. Subsumption can be defined relative to given first-order clausal background theory, (see Clausal Form). In this case, clause relatively subsumes clause whenever . Plotkin studies the case in which is taken to be Resolution-based derivation in which each clause in
is used at most once. In this case there exists a unique relative least general generalisation (rlgg), of two clauses
and . In Muggleton (1991) it is shown that the relative subsumption lattice is the same as the lattice searched by Inverse Resolution. More specifically the most specific inverse resolvent to depth is unique up to renaming of variables. The least general generalisation of the most-specific inverse resolvents of and is equivalent to the relative least general generalisation of and .
- Muggleton, S., Inductive Logic Programming New Generation Computing 8 (1991) no.4, 295--318.