Re: same-syntax extensions to RDF

> > 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.

I supppose this is part of why I'm asking your help here.  It's not at
all clear to me how to go about expressing this design in the style of
the RDF MT.   Maybe we can keep going on the other details and return
to this point if we're clear on the others?   I might be able to
figure out a design in this style if I stare at it long enough.

> > 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?

It's a semantic condition on all interpretations.   In my
implementation, it's one of the formulas to throw into the KB before
querying, to help you get the full results you'd expect.

> > > > 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 t
> he
> > > 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.

As with "capturing" FOL, I'm not sure what that means.   I want to
stuff FOL formulas down an RDF pipe and have them come out the other
end in good working order, as in this test case:

> > 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.

It does support that.   Those example are fine.

Well, I guess it really depends on the API and whether "the system" is
trying to be an entailment checker, a query answering service, a
consistency checker, an inconsistency checker, etc, ....   but I don't
see any particular problems with the query-answering use case.   


> > > > 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 tha
> t
> > > 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.

Sure, but the entailments are not in the reified form, they are in the
ordinary de-refied form.   

In KIF-like syntax:

   (Usable (r a b))
entails
   (r a b)

and
   (Usable (and (r a b) (r c d)))
entails
   (and (r a b) (r c d)))
which of course entails
   (r a b)
and
   (r c d)

The goal, again, is for someone to be able to express the definition
of fam:uncle in RDF in a way which supports the obvious inferences and
causes no serious problems.    If it's not clear yet how this design
does that, what would help clarify it?

    -- sandro

Received on Friday, 17 December 2004 20:56:12 UTC