Re: AS & S Review: Appendix A.1: Correspondence between Abstract OWL and OWL DL

From: herman.ter.horst@philips.com
Subject: AS & S Review: Appendix A.1: Correspondence between Abstract OWL and OWL DL
Date: Thu, 23 Jan 2003 15:14:44 +0100

> 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.

I believe that the development in the document is now internally
consistent.  Further, I believe that the document corresponds as closely as
possible to the Last Call version of the RDF Semantics document.  (There
are errors in the RDF Semantics document, which make completely
correspondence infeasible.)  In particular I believe that the document does
in fact correspond to the RDF Semantics document with respect to CI/CEXT.

Multiple changes have had to be made to the definitions in the document,
and to the proof, to keep up with changes in the RDF model theory.  Due to
these many changes at certain times the document was not internally
consistent.  I believe that needed fixes to the RDF model theory will
require further changes to the document.

Because of the problems with the RDF model theory, many of which I had
pointed out before the RDF Core WG went do last call, I do not see a good
way in which this document can go to last call before a new version of the
RDF model theory has been published.  My understanding is that the RDF
model theory is now officially frozen, due to last-call process
requirements, so it may be a while before a new version of the RDF model
theory is available.

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

Actually, annotations were added at the very last minute, so I don't see
how they could be relevant from the beginning.  Admittedly the situation
with respect to imports is annoying.  Imports brings in issues having to do
with documents and names of ontologies, which have not been handled very
well, even in DAML+OIL.  I may have a way around this, which builds on the
recent proposed changes I made to the abstract syntax and direct semantics.

> 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".

I agree that the proofs are very compact.  If someone has time, feel free
to expand on them.

> 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.)

Yes, I think that this is a problem in the Lemma.  I'll work on it.

> 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.

This needs fixing, I'll work on it.

> The statement of Theorem 1 in Section 5 includes
> "and let V = V' union ...", while V is not used in
> that statement.

This phrase can just be removed.

> 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')"

This is not a typo.

> There is often KB or knowledge base instead of ontology.

Fixed.

> There is often an n for a vocabulary element instead
> of v.

I'll look for this.

> Typo in proof of Lemma 4: VOP u VDP

I can't find this, maybe I already fixed it.

> In the proof of Lemma 1: a "cup" instead of a union.

I can't find this, maybe I already fixed it.

> Herman ter Horst
> Philips Research

peter

Received on Saturday, 8 February 2003 09:39:54 UTC