- From: pat hayes <phayes@ai.uwf.edu>
- Date: Mon, 24 Feb 2003 14:33:50 -0600
- To: herman.ter.horst@philips.com
- Cc: www-rdf-comments@w3.org
>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.
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.
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
Received on Monday, 24 February 2003 15:34:25 UTC