- 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