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

Date: Thu, 23 Jan 2003 15:14:44 +0100

To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>

Cc: www-webont-wg@w3.org

Message-ID: <OF6D540C0C.599AA456-ON41256CB7.003F5881-C1256CB7.004E6DCB@diamond.philips.com>

Date: Thu, 23 Jan 2003 15:14:44 +0100

To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>

Cc: www-webont-wg@w3.org

Message-ID: <OF6D540C0C.599AA456-ON41256CB7.003F5881-C1256CB7.004E6DCB@diamond.philips.com>

Review comments for Abstract Syntax and Semantics Appendix A.1: Correspondence between Abstract OWL and OWL DL Version of 17 January This appendix gives the proof that the abstract OWL syntax and semantics can be realized as a semantic extension of RDFS, in the way described in Section 5. Although only informative, and although it will not be widely read, it is a vital part of the document as it confirms the connection between the official semantics level of OWL (which is in terms of the abstract syntax) and the official exchange syntax level of OWL (which is RDFS). Today my review of the AS & S document is due, but I cannot yet confirm that the result in this appendix is correct on the basis of its proof. One point is that developments in the earlier part of the document cause the need for changes in the proof, and this does not stimulate the complete reading of this proof. This holds, in particular, for the definition of RDF interpretation, which needs to add PI, and the discussion on CI/CEXT. The correspondence is not proved in general, but only without annotations and imports. The following sentence seems odd: "Actually, a slightly stronger correspondence can be shown, but this is enough for now, as the presence of annotations and imports causes even more complications." Annotations and imports are relevant from the beginning, when will it be relevant to include annotations and imports in the proof? One of the main comments I want to make about this appendix is that the text is too condensed to be considered sufficiently well readable. Semantic extensions of RDF is a new subject for everyone. The problem is not that very many cases in the proofs just consist of the word "similar", this is normal. The problem is more that, especially in Lemmas 1 and 2, the cases that are treated could use more detail, should be provided with more "stepping stones". For example, in connection with Lemma 4 there is a subtle point that although many CEXTI values are stated, these should be used in combination to define the value EXTI(SI(rdf:type)). In connection with the Lemma 1, it would be helpful to note that when going from I to I+E, one does not need to take CEXTI+E(I+E(...)), but one can take CEXTI(I+E(...)). This does not need to be proved, but could be noted explicitly. (By the way, the statement of Lemma 1 has an error: in the three numbered conclusions, it should be CEXTI(I+E(M(T(d)))) instead of CEXTI(I(M(T(d)))), as the M(T(D)) values will quite generally be blank nodes.) To give another example of a place where more information would be helpful, consider the first case of Lemma 2. In the second paragraph it is stated "Because I satisfies T(V)" where it is known that I is an interpretation of V. In the third paragraph, the word "Thus" also is a step where the reader needs to fill in a lot. Many other examples of the need for further details can be given. I remember that Peter said in a telecon when he had just finished this proof that he could not imagine that anybody would read this. What this text could use very well is another editing round, wherein it is imagined that the text is read by other people. I do not think that this would need to lead to very much additional text. == Other comments about Appendix A.1: The statement of Theorem 1 given in this appendix differs slightly from that in Section 5. In Section 5, the T(V') part is missing: it should be added there as well. The statement of Theorem 1 in Section 5 includes "and let V = V' union ...", while V is not used in that statement. When T(V') is introduced, it should be noted that this is an extension of the mapping in Section 4: Section 4 does not define the value of T for a vocabulary element (a URI). It is convenient that the definitions of separated OWL vocabulary and separated names are recalled: it is however confusing that these are stated here in the appendix for V instead of V': in Lemma 1 they appear with V' instead of V (also in Section 5 they appear with V' instead of V). Typo in statement of Lemma 1: "of V of T(V')" There is often KB or knowledge base instead of ontology. There is often an n for a vocabulary element instead of v. Typo in proof of Lemma 4: VOP u VDP In the proof of Lemma 1: a "cup" instead of a union. Herman ter Horst Philips ResearchReceived on Thursday, 23 January 2003 09:16:52 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 7 December 2009 10:57:57 GMT
*