Re: RDF Semantics: subinterpretations

Pat,

Thank you for your comments.

>>RDF Semantics document,
>>last call version, 23 january 2003
>>This comment was mailed earlier to the WebOnt WG [1].
>
>For the record, the editor accepts this as an editorial comment.
>
>>The definition of subinterpretation I << J in Appendix B
>>is not clear, as
>>it is not clear what a "projection mapping from IR into JR,
>>IS into JS, IL into JL and IEXT into JEXT" is.
>>IR and JR are sets, so the first part is clear: a function
>>from IR into JR. However, IS and JS are functions.
>>(What is meant by a mapping from a function to a function?)
>
>The concept is a familiar one in mathematics: it is often referred to 
>as a morphism between functional categories.

I am familiar with category theory and with how morphisms
between [objects in] functional categories are typically defined.
Because the details of this can vary and were not completely
determined by what you wrote, I made my comment.
For the description of the definition I gave below I was
inspired by examples from category theory.
In fact, this definition can be interpreted as making a category out 
of the interpretations of an RDF graph.

>
>But the wording of the proofs of lemmas will be clarified and this 
>definition made more explicit.
>
>>It seems that the following definition suits the intended
>>use in the Herbrand lemma:
>>
>>I is a subinterpretation of J, I << J, when there is a projection
>>mapping f : IR -> JR such that the following hold:
>>- f(IP) subsetof JP  [this is needed for the last condition]
>>- for each v in V, JS(v)=f(IS(v))
>>- for each typed literal l, JL(l)=f(IL(l))
>>- for each p in IP,
>>{ <f(x),f(y)> : <x,y> in IEXT((I(p)) } subsetof JEXT(f(p))
>>
>>Then, automatically, the property that is desired in the text
>>follows: any triple is true in J if it is true in I.
>
>Yes, quite, that is the intent of the current phrasing, stated in a 
>lengthier form.
>
>There is an editorial issue generally in writing such things as this 
>appendix. In many people's view, a document like this should not even 
>have things like lemmas and proofs in it *anywhere*. To anyone 
>trained in formal logic these results and the proof techniques are 
>all elementary in any case. On balance, therefore, it seemed 
>appropriate to give an expository outline of the basic proof 
>techniques as an informative guide for some readers as well as 
>providing others (such as yourself, Herman) with the opportunity to 
>check the reasoning. However, to write out these proofs too formally 
>and in too much detail does not seem appropriate, as this would make 
>them unreadable by the novice and boring to the initiated.
>
>I will try to make the wording clearer, however, in the light of your 
comments.

You integrate in one sentence two statements 
(too formally / too much detail) about two
kinds of reader here (novice / initiated).
It seems that the novice is helped by detail.
It should not be too formal for the novice.  For example, I agree that
mentioning categories, as we just discussed above, in this document would 
not be appropriate:  in this case more details should be spelled out.
Having this material in the document may help people who are not
formal logicians to become convinced to use RDF in projects.
After all, the normative definition of entailment is highly 
theoretical, and this appendix supports a more practical,
triple-based characterization of entailment.

As to the initiated, I would like to make the following comment.
In spite of the fact that elementary, well-known techniques are
involved in the proofs, and in spite of the fact that the field of
logic has successfully investigated much more complicated situations,
it seems that the entailment results in this appendix do not all 
follow directly from existing results in the field of logic. 
Correct me if I'm wrong.  Even if all these results would follow
directly from existing results in logic, there is value in
collecting stand-alone proofs such as described in the document.
However, it seems that some new territory is involved, and 
there is definitely some degree of complexity, and therefore proofs 
have to be provided *somewhere*.


>
>Pat
>-- 
>---------------------------------------------------------------------
>IHMC  (850)434 8903 or (650)494 3973   home
>40 South Alcaniz St.                                            (850)202 
4416   office
>Pensacola               (850)202 4440   fax
>FL 32501             (850)291 0667    cell
>phayes@ai.uwf.edu                         http://www.coginst.uwf.edu/~phayes
>s.pam@ai.uwf.edu   for spam
>
>

Herman

Received on Wednesday, 26 February 2003 11:17:38 UTC