Re: Datalog With Only Binary Relations Is Too Weak

> [Sandro]
> [ rdf-logic: This e-mail is continuing a face-to-face conversation
> Benjamin Grosof and I were having yesterday.  I'm trying to understand
> how KR language expressiveness theory applies to RDF.  Others are
> welcome to join, of course. ]
>
> Okay, this morning my brain is properly in gear.
>
> Let's say we want to capture the grandparent relation.  Intuitively we
> know grandparent(a,c) means something like parent(a,b) and
> parent(b,c).  But how do we write this?
>
> One direction is easy:
>     grandparent(?a, ?c) <--- parent(?a, ?b) and parent(?b, ?c)
>     parent(gregorian, sandro)
>     parent(sandro, bret)
> we can now infer: grandparent(gregorian, bret).
>
> But what if we're given
>     grandparent(gregorian, bret)
>     isLoved(?x) <---- parent(?x, ?y)
> and we'd like to prove isLoved(gregorian)?
>
> In FOL you can say
>     forall a
>       forall c
>         grandparent(a,c) implies
>            exists b suchthat
>               parent(a, b) and
>               parent(b, c)
>
> In NILE you say
>      rule "" ($a grandparent $c ==> $a parent !b; !b parent $c)

I have to learn NILE asap, any pointer Sandro?

> In Prolog (but not Datalog) you can say:
>      parent(X, parent_of(X)) :- grandparent(X, Y).

Well, I must have forgotten about _of, how is Y unified?

> In Prolog or Datalog you can rephrase in terms of a 3-ary relation:
>     gen3(X,Y,Z) :- parent(X,Y), parent(Y,Z).
>     parent(X,Y) :- gen3(X,Y,Z).
>     parent(Y,Z) :- gen3(X,Y,Z).
> which lets us rephrase our test case:
>     gen3(gregorian, whatever, bret).
>     isLoved(X) :- parent(X, Y).
> and then infer isLoved(gregorian) as we want.   (In practice, this
> set of rules puts prolog into a loop, although XSB should handle it
> with tabling.)
>
> But how else?

... what can we say here?

{{:X :grandparent :Z} log:implies {:X :parent :Y}} log:forAll :X, :Y, :Z.
{{:X :parent :Y} log:implies {:X a :isLoved}} log:forAll :X, :Y.
:gregorian :grandparent :bret.

this is expressed in n3 (and definite but not complete)
if we now now ask

{:X a :isLoved} log:forAll :X.

we get (using euler proof mechanism)

 {{:gregorian :grandparent :bret} log:implies
  {:gregorian :parent :Y}} log:implies
{:gregorian a :isLoved}.

(have to think about quantifying that :Y ...)

> And thus my hypothesis: datalog with only binary predicates is too
> weak to talk about transitive relations.

Maybe, maybe not ... I just don't know it for the moment (missing some gear :-)
There is no problem if we add
{{:X :parent :Y. :Y :parent :Z} log:implies {:X :grandparent :Z}} log:forAll :X, :Y, :Z.
or some other kind of redundancy (whis is a good thing to have ...)

>    -- sandro

-- Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Received on Friday, 16 March 2001 09:54:49 UTC