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 ).