- From: <jos.deroo.jd@belgium.agfa.com>
- Date: Sat, 17 Mar 2001 16:45:49 +0100
- To: phayes@ai.uwf.edu, Sandro@w3.org
- Cc: Steve_Cayzer@hplb.hpl.hp.com, www-rdf-logic@w3.org
> [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/
Received on Saturday, 17 March 2001 10:46:10 UTC