- From: pat hayes <phayes@ai.uwf.edu>
- Date: Fri, 16 Mar 2001 16:57:03 -0600
- To: "Cayzer, Steve" <Steve_Cayzer@hplb.hpl.hp.com>
- Cc: www-rdf-logic@w3.org
>Forgive the obvious point, but surely
> grandparent(?a, ?c) <--- parent(?a, ?b) and parent(?b, ?c)
>only works one way?
>So you'd actually want some sort of definition (or implication the other
>way) as Jos said
> {{:X :grandparent :Z} log:implies {:X :parent :Y}} log:forAll :X,
>:Y, :Z.
>
>I tried something similar in XSB
> parent(X,Y) :- grandparent(X,Z).
>before I realised that because Y isn't quantified, of course this means that
>XSB will happily infer that grandparents are parents of anybody you choose
>to name.
>Oh, and also XSB started cycling having the 2 rules there.
>
>Surely all we want is Y as a skolem constant?
>Perhaps there's some simple way to do that in datalog? (he asks hopefully)
I have no idea about datalog, but its not a Skolem function, not a
skolem constant.
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.
Pat Hayes
---------------------------------------------------------------------
IHMC (850)434 8903 home
40 South Alcaniz St. (850)202 4416 office
Pensacola, FL 32501 (850)202 4440 fax
phayes@ai.uwf.edu
http://www.coginst.uwf.edu/~phayes
Received on Friday, 16 March 2001 17:55:34 UTC