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.

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

[...]

> > Your first task should be to demonstrate that the encoding of a conjunction
> > follows from the encoding of its conjuncts. 
>                ^^^^^^^^^^^^^^^
> 
> I'm not sure if you were trying to repeat the above issue here, or
> have this be a different one.  

Somewhat of a repeat, as the two should be quite closely related, ...

> Following from the reified and asserted
> form of the conjuncts is quite different from following from the
> conjuncts.

but you probably need both.  (You could just do FOL in the encoding and
divorce it from the unencoded facts, but I don't think that you want to.)

> 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 lx:conjLeft _:left.
>    _:x lx:conjRight _:right.
>    _:left lx:subjectTerm _:lefts.
>    _:left lx:predicateTerm _:leftp.
>    _:left lx:objectTerm _:lefto.
>    _:lefts lx:denotation <a>.
>    _:leftp lx:denotation <r>.
>    _:lefto lx:denotation <b>.
>    _:right lx:subjectTerm _:rights.
>    _:right lx:predicateTerm _:rightp.
>    _:right lx:objectTerm _:righto.
>    _:rights lx:denotation <c>.
>    _:rightp lx:denotation <r>.
>    _:righto lx:denotation <d>.
>    _: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.

> Is this the right track?   If so, I'll continue to address the points
> you raise in the previous e-mail.

This is at least addressing my issues.

>        -- sandro

peter

Received on Thursday, 16 December 2004 15:12:45 UTC