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

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 Research