Re: same-syntax extensions to RDF

From: Sandro Hawke <sandro@w3.org>
Subject: Re: same-syntax extensions to RDF 
Date: Thu, 16 Dec 2004 12:30:51 -0500

> > From: Sandro Hawke <sandro@w3.org>
> > Subject: Re: same-syntax extensions to RDF 
> > Date: Thu, 16 Dec 2004 09:29:35 -0500

[...]

> Is it important that I express these in the same form as you used in
> S&AS 5.2 (subsection "Comprehension conditions (principles)")?
> 
> For instance, where you say 
> 
>    If there exists
>    ======================
>    x1, ... xn in IOC
> 
>    Then there exists I1, ..., IN in IL with
>    ========================================
>    <I1,x1> in EXT1(S1(rdf:first)), ....
> 
> I'd be much happier saying
> 
>    rdf(rdf_nil, rdf_type, rdf_List).
>    % all lists of all things exist
>    all X L1 (
>       rdf(L1, rdf_type, rdf_List)
>       ->
>       exists L2 (
>          rdf(L2, rdf_type, rdf_List) &
>          rdf(L2, rdf_first, X) &
>          rdf(L2, rdf_rest, L1)
>       )
>    ).
> 
> Is that okay?  For me, it has two huge advantages: I can run automated
> test cases against it, and I have an off-the-shelf reference
> implementation available.  (I'm using Otter here, but Vampire or any
> other FOL Theorem Prover should basically work.)

Hmm.  You might get in trouble by assuming that too much machinery
underlies the comprehension principles or using the wrong context.  In any
case, the goal is to make an extension of the RDF model theory, so you
should really stay very close to the methods used there, which is why the
OWL comprehension principles are stated the way they are.

> In this form, the comprehension principle needed above seems rather
> straightforward:
> 
>    all A R B (
>       rdf(R, rdf_type, rdf_Property)
>       ->
>       ( exists SubjTerm PredTerm ObjTerm Triple (
>            rdf(Triple, rdf_type, lx_Triple) &
>            rdf(Triple, lx_subjTerm, SubjTerm) &
>            rdf(Triple, lx_predTerm, PredTerm) &
>            rdf(Triple, lx_objTerm, ObjTerm) &
>            rdf(SubjTerm, lx_denotation, A) &
>            rdf(PredTerm, lx_denotation, R) &
>            rdf(ObjTerm, lx_denotation, B) 
>       ))
>    ).

What do A, R, and B range over?  Is this a formula that is true in an
interpretation or is it a semantic condition on interpretations?

> > > but the 8th, by
> > > design, is not.  Usability is not implied by truth.
> > 
> > > Do you see a problem with this bit?  Do you want the 8th triple to be
> > > entailed as well for some reason?
> > 
> > Yes indeed.  The first seven triples may be entailed by the empty KB, if
> > you get the comprehension principles right, but somehow you need to get the
> > connection between.
> > 
> >     <a> <r> <b> .
> > 
> > and the truth of the encoding of the sentence R(a,b).   Otherwise how can
> > you say that you have captured FOL?
> 
> By design, Usable only goes one way.  So there's a connection, but not
> an if-and-only-if connection.   

But if there is no if-and-only-if then you really don't have logic.

> I'm not quite sure what it would mean to "capture" FOL, so I'll be
> more specific. 
> 
> I want people to able to publish FOL assertions in RDF on the web so
> others can aggregate them (using RDF harvester/aggregators) and draw
> the normal FOL conclusions.   
> 
> For instance
>    e:yeshayah fam:brother e:sandro.
> from one source,
>    e:yeshayah fam:daughter e:eliana.
> from another source, and suitable definitions expressed at the fam:
> namespace in LX triples should allow one to conclude
>    e:eliana fam:uncle e:sandro.

Yes sure, but what happens if I assert (using your machinery)
    ( <a> <r> <b> . ) & ( <c> <r> <d> . )
and some one else asks whether 
    ( <c> <r> <d> . ) & ( <a> <r> <b> . )
follows from this?  Or, and more difficult to get right, what happens 
if I assert (using your machinery)
   A x ( <a> <r> x . )
and some one else asks whether 
    <a> <r> <b> .
follows?

If your formal machinery doesn't support this then it really hasn't
captured logic at all.



> > > Here I think you're asking whether
> > >    for some _:SA_left, _:SA_lefts, _:SA_leftp, _:SA_lefto
> > >    _:SA_left lx:subjectTerm _:SA_lefts.
> > >    _:SA_left lx:predicateTerm _:SA_leftp.
> > >    _:SA_left lx:objectTerm _:SA_lefto.
> > >    _:SA_lefts lx:denotation <a>.
> > >    _:SA_leftp lx:denotation <r>.
> > >    _:SA_lefto lx:denotation <b>.
> > >    _:SA_left rdf:type lx:Usable.
> > > and
> > >    for some _:SA_right, _:SA_rights, _:SA_rightp, _:SA_righto
> > >    _:SA_right lx:subjectTerm _:SA_rights.
> > >    _:SA_right lx:predicateTerm _:SA_rightp.
> > >    _:SA_right lx:objectTerm _:SA_righto.
> > >    _:SA_rights lx:denotation <c>.
> > >    _:SA_rightp lx:denotation <r>.
> > >    _:SA_righto lx:denotation <d>.
> > >    _:SA_right rdf:type lx:Usable.
> > > together entail
> > >    for some _:x, _:left, _:lefts,  _:leftp,  _:lefto
> > >                  _:right , _:rights,  _:rightp,  _:righto
> > >    _:x rdf:type lx:Conjunction.
> ...
> > >    _:x rdf:type lx:Usable.
> > > 
> > > which I believe I can show.  
> >
> > Well, yes, I would like to see how this works.  I didn't see anything that
> > gives me reason to believe that it does follow, however.  In particular I
> > don't see anything in the rationale for Usable that could lead to the
> > possiblity of inferring that Usable was the type of any resource.
> 
> You're right, I was overly hasty in thinking that entailment held.  We
> don't need it for my use cases, and to provide for it gets problematic


See above.

The ability to derive consequences is the heart of a logic.  If you can't
get FOL entailment from your machinery you haven't done FOL.

>        -- sandro


peter

Received on Thursday, 16 December 2004 23:35:46 UTC