Re: same-syntax extensions to RDF

> From: Sandro Hawke <sandro@w3.org>
> Subject: Re: same-syntax extensions to RDF 
> Date: Thu, 16 Dec 2004 09:29:35 -0500
> 
> > 
> > > In your formalization does
> > > 	a r b .
> > > 	c r d .
> > > entail the encoding of the conjunction of a r b . and c r d . ?
> > 
> > It looks like you are asking whether 2 RDF triples entail the ~20
> > triples which describe and assert those same triples as an
> > lx:Conjunction.  A simpler case would be whether 1 RDF triple entails
> > the ~8 triples which describe and assert that triple via LX.
> > 
> > Specifically, for example, does
> >    <a> <r> <b>.
> > entail (for some _:x)
> >    _:x rdf:type lx:Triple.
> >    _:x lx:subjectTerm _:xs.
> >    _:x lx:predicateTerm _:xp.
> >    _:x lx:objectTerm _:xo.
> >    _:xs lx:denotation <a>.
> >    _:xp lx:denotation <r>.
> >    _:xo lx:denotation <b>.
> >    _:x rdf:type lx:Usable.
> > 
> > The first 7 triples are entailed by the empty KB, 
> 
> Hmm.  I think that I'm missing something then.  How is 
> 
>    _:x rdf:type lx:Triple.
> 
> entailed by the empty KB?  You have claimed this, but given not even a hint
> of how it is going to happen.  There are pitfalls here, and you need to
> give some outline of how these comprehension principles work.

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

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



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

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.


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

       -- sandro

Received on Thursday, 16 December 2004 17:27:53 UTC