Catalogue of Artificial Intelligence Techniques


Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML

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 .



Add Comment

No comments.