Abstract Syntax and Semantics: review comments

Abstract Syntax and Semantics: 
review comments about version of 19 December

This is not a complete review, but mainly a summary of points left 
open from my earlier partial review at [1].  Most of these points 
express a desire to extend the document with additional information.

- Correspondence between OWL DL entailment and OWL Full entailment.
The Bristol consensus on semantics already expressed the need for a 
characterization of the situation that DL and Full (in those days, fast
and large) entailment coincide [2].  There is now an informative appendix
with a brief sketch in this direction.
I do not understand how the theorem given there follows from the lemma.
It does not seem to follow from the statement of the lemma alone: if I is 
an
OWL Full interpretation that satisfies K, then it needs to be proved that
I satisfies C.  Getting another OWL DL interpretation I' that 
satisfies K, shows that I' satisfies C.  And then?

Until we can really view the lemma and the theorem and its converse 
as proved, we do not really know about the correspondence between 
OWL DL entailment and OWL Full entailment.

- The entailment definitions in the document are theoretical, 
in terms of models.
It would be useful to have more practically useful, triple-based 
characterizations of entailment, as in the RDF Semantics document [3].
As long as such characterizations remain unknown, 
a sequence of simple sufficient conditions for entailment (i.e., simple 
inference rules, formally stated, with proofs of validity) could 
form a useful informative addition to the document in order to 
familiarize people with the various kinds of OWL entailment. 

 - It would also be nice to know how an OWL DL KB is characterized in 
triple form.  That is, what is an "OWL DL graph" as a special kind of 
RDF graph?

- The document gives three definitions of OWL entailment (abstract, 
DL en Full) but what is the normative definition of OWL entailment?. 
The consensus summary said that in case of disagreement between 
DL (fast) and Full (large) entailment, DL entailment is normative [2]. 
In the new version, Peter introduced the
words "authorative" (for the direct model theory) and "secondary" 
(for the RDFS-compatible model theory) in the document. 
I think the word normative should be used.

- Section 2.1: A small simplification is possible: use the two rules for 
<annotation> also in <directive>, instead of their content. 

- 5.2: In the tables defining the cardinality restrictions: 
instead of card({v:<u,v>...) make it completely explicit with the set 
from which v can be taken:  card({v elementOf ...:<u,v>...) 

Herman ter Horst 
Philips Research 

[1] http://lists.w3.org/Archives/Public/www-webont-wg/2002Nov/0043.html 
[2] http://lists.w3.org/Archives/Public/www-archive/2002Oct/0022.html 
[3] http://www.w3.org/TR/2002/WD-rdf-mt-20021112/