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
.
References:
- Muggleton, S., Inductive Logic Programming New Generation Computing 8 (1991) no.4, 295--318.
Comments:
No comments.