Slide 14.7: Examples of Horn clauses (cont.)

Slide 14.6: Examples of Horn clauses
Slide 14.8: Resolution
Home

Examples of Horn Clauses (Cont.)

Example II
The foregoing examples contain only universally quantified variables. This example shows how to handle an existentially quantified variable:

   x is a grandparent of y if
     x is the parent of someone who is the parent of y.

Translating this into first-order predicate calculus, we get

   for all x, for all y,
     ( there exists z, parent( x, z ) and parent( z, y ) )
 → grandparent(x, y).

As a Horn clause this is expressed simply as

   parent( x, z ) and parent( z, y ) → grandparent( x, y ).

Example III
This example shows how to remove “or” connectives by writing separate clauses. Also, assume that the result clauses have the following features:

the variables appearing in the right-hand side (head) of the symbol ‘→’ is universally quantified, and
the variables appearing in the left-hand side (body) of the symbol ‘→’, but not in the head, is existentially quantified.

   For all x, if x is a mammal then x has two or four legs.

Translating this into predicate calculus, we get

   for all x, mammal( x ) → legs( x, 2 ) or legs( x, 4 ).

This may be approximated by the following Horn clauses:

   mammal( x ) and not legs( x, 2 ) → legs( x, 4 ).
   mammal( x ) and not legs( x, 4 ) → legs( x, 2 ).