RE: Datalog With Only Binary Relations Is Too Weak

> [Pat]
> 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.

... OK, let's try that skolem stuff with n3 (I never _did_ that so far ...)

   @prefix log: <http://www.w3.org/2000/10/swap/log.n3#>.
   @prefix : <#>.

   {{:X :parent :Y. :Y :parent :Z} log:implies {:X :grandparent :Z}} log:forAll :X, :Y, :Z.

   {{:X :grandparent :Z} log:implies {:X :parent {:X :skolemfun :Z}}} log:forAll :X, :Z.
   {{:X :grandparent :Z} log:implies {{:X :skolemfun :Z} :parent :Z}} log:forAll :X, :Z.

   {{:X :parent :Y} log:implies {:X a :isLoved}} log:forAll :X, :Y.

   :gregorian :grandparent :bret.

and let's now try to find an answer to the lemma

   @prefix log: <http://www.w3.org/2000/10/swap/log.n3#>.
   @prefix : <parent.n3#>.

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

oops ... we go in an infite loop ... %$#@!
I can see why, but it's too late in the night ...
wake up, look to F1 qualifation, good gear and
*improve cycle detection with unify method*
(instead of the equals method)
[i'm actually talking about http://www.agfa.com/w3c/euler/ ]
it's also simpler and faster now ... @@ theory
and we get the answer

   @prefix log: <http://www.w3.org/2000/10/swap/log.n3#>.
   @prefix : <http://vam969//parent.n3#>.

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

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

   # Proof found in 15 steps (4267 steps/sec)

so 2 solutions and some skolemfun :-)
I try to find evidence that having (nested) dyadic formulae
is a good thing to limit to ...

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