RE: Datalog With Only Binary Relations Is Too Weak

>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