From: <herman.ter.horst@philips.com>

Date: Wed, 26 Feb 2003 17:15:41 +0100

To: pat hayes <phayes@ai.uwf.edu>

Cc: www-rdf-comments@w3.org

Message-ID: <OF4E726EAE.353A18D4-ON41256CD9.00510269-C1256CD9.00597DAF@diamond.philips.com>

Date: Wed, 26 Feb 2003 17:15:41 +0100

To: pat hayes <phayes@ai.uwf.edu>

Cc: www-rdf-comments@w3.org

Message-ID: <OF4E726EAE.353A18D4-ON41256CD9.00510269-C1256CD9.00597DAF@diamond.philips.com>

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 > > HermanReceived on Wednesday, 26 February 2003 11:17:38 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Friday, 21 September 2012 14:16:31 GMT
*