Re: same-syntax extensions to RDF

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


> 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.  Following from the reified and asserted
form of the conjuncts is quite different from following from the
conjuncts.

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.  

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

       -- sandro

Received on Thursday, 16 December 2004 14:26:37 UTC