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, l1 and l2 is θ . Thenl1θ=l2θ

is called the most general instance (mgi) ofl1

and l2 . Like the most general instance, the least general generalisation (lgg) of l1 and l2 does not always exist. However, whenever l1 and l2 have the same predicate symbol and sign their lgg is unique up to renaming of variables. Generalisation over literals is defined by subsumption. l1 subsumesl2

whenever there exists a substitution θ such thatl1θ=l2

. 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, B (see Clausal Form). In this case, clause C relatively subsumes clause D whenever BCD . Plotkin studies the case in which is taken to be Resolution-based derivation in which each clause inBC

is used at most once. In this case there exists a unique relative least general generalisation (rlgg), C of two clauses D1

and D2 . 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 n is unique up to renaming of variables. The least general generalisation of the most-specific inverse resolvents of D1 and D2 is equivalent to the relative least general generalisation of D1 and D2 .


References:


Comments:

Add Comment

No comments.