- From: Drew McDermott <drew.mcdermott@yale.edu>
- Date: Mon, 19 Mar 2001 13:56:25 -0500 (EST)
- To: www-rdf-logic@w3.org
[Pat Hayes:]
The logical form of this is (in KIF: the connectives come before the
things they connect rather than in between them):
(forall (?a ?c)( <=> (grandparent ?a ?c)
(exists (?b)(and (parent ?a ?b)(parent ?b ?c)))
))
which skolemises to:
(forall (?a ?c)( <=> (grandparent ?a ?c)
(and (parent ?a (f ?a ?c))(parent (f ?a ?c) ?c)))
))
The skolem function f(x,y) is the (hopefully unique) parent of y who
is x's child.
This is not quite right. The problem is that p <=> q is short for
(and (=> p q) (=> q p)). The existential appears negated in one of
the conjuncts. So the proper skolemized form is:
(and (=> (and (parent ?a ?b) (parent ?b ?c))
(grandparent ?a ?c))
(=> (grandparent ?a ?c)
(and (parent ?a (f ?a ?c))
(parent (f ?a ?c) ?c))))
Note that the first conjunct is what Sandro wrote to begin with.
Sandro also posed the following problem:
But what if we're given
grandparent(gregorian, bret)
isLoved(?x) <---- parent(?x, ?y)
and we'd like to prove isLoved(gregorian)?
From the first premise we infer (parent gregorian (f gregorian bret))
and (parent (f gregorian bret) bret). Then we use Sandro's second
premise plus (parent gregorian (f gregorian bret)) to conclude
isLoved(gregorian).
If we want all backward chaining we express the skolemized form as
(<-- (grandparent ?a ?c)
(and (parent ?a ?b) (parent ?b ?c)))
(<-- (parent ?a (f ?a ?c))
(grandparent ?a ?c))
(<-- (parent (f ?a ?c) ?c)
(grandparent ?a ?c))
Any backward-chaining algorithm will solve this one.
-- Drew McDermott
Received on Monday, 19 March 2001 13:56:27 UTC