===================================================================== Review for "OWL 2 Web Ontology Language -- Model-Theoretic Semantics" ===================================================================== revision 12088: http://www.w3.org/2007/OWL/wiki/index.php?title=Semantics&oldid=12088 Summary ------- This document is technically correct, except for a few repairable inconsistencies. In addition, I have several issues concerning notation and expression, some of the latter arising in connection with readability for non-experts. Specific comments ----------------- * 1 Introduction - 2nd sentence: This is difficult to read. Strictly speaking, semantics is a different kind of object than its definition or even a DL. Consequently, you can't compare semantics with definition principles or with SROIQ. This remark might seem pedantic, but it shows that the sentence is just not fluid enough for an intro. How about this: It [this document] follows the principles for defining the semantics of description logics and largely adopts the formalism underlying the description logic SROIQ. - 5th sentence: *a* core part? And again, semantics equivalent to the definition of a language? - Apart from the two above comments, I find the motivation/justification of the pursued approach strong and helpful. * 2.1 Vocabulary - Definition of N_{DT}: This is inconsistent with the OWL 2 Specification: in Section 4 [ http://www.w3.org/2007/OWL/wiki/Syntax#Datatype_Maps ] , it says that N_DT *must not* contain rdfs:Literal. - Currently, this document contains 'data type' (e.g., in this subsection) and 'datatype' (in the following subsection). * 2.2 Interpretations - Definition of Delta_D: The notion (DT)^{DT} is very confusing. Please don't use 'DT' for different things (datatype and superscript of the interpretation function). One of these can be replaced, e.g., by the lower case symbol 'dt'. The same for ''OP'', ''DP'', ... -- and, of course, in the Syntax document. - Definition of .^C: If {owl:Thing, owl:Nothing} is a subset of N_C, why are they excluded in the definition of .^C? If they are meant to be class *expressions* (because they appear in Table 4), then they shouldn't be in N_C. On the other hand, if they are meant to be in N_C, then they shouldn't be excluded here, but be removed from Table 1. The same remark for owl:TopObjectProperty/owl:BottomObjectProperty and owl:TopDataProperty/owl:BottomDataProperty, the latter of which would make Section 2.2.2 redundant. * 2.2.3 Data Range Expressions - The rest of this section speaks of 'data ranges', so the section should be named 'Data Ranges' as well? * 2.2.4 Class Expressions - Third table entry -- extremely tiny issue: Wouldn't it be a tad more consistent with the order within Section 8.1 of the Syntax document [ http://www.w3.org/2007/OWL/wiki/Syntax#Propositional_Connectives_and_Nominals ] if 'ComplementOf' appeared after 'UnionOf'? * 2.3 Satisfaction in an Interpretation - Second sentence: This is the first time 'axiom closure' occurs in this document. It should be defined here, or the reader should be referred to Section 3.4 of the OWL 2 Specification. [ http://www.w3.org/2007/OWL/wiki/Syntax#Imports ] - Second sentence again: I would like to see a sentence here which explains that . ISNAMED is only necessary for (and used in) defining the semantics of KeyFor axioms and . that this makes it necessary to refer to O in the definition of the satisfaction of axioms. Otherwise, readers might stumble over the use of ISNAMED here and 'w.r.t. O' in the following subsections. * 2.3.2 Object Property Expression Axioms - Second table entry: I think here and in other rows of this and the following tables, 'imply' needs to be replaced by 'implies': This statement has the form '(a_1 & ... & a_n) => c', where 'a_1 & ... & a_n' is a *single* composite statement that impl*ies* c. The current reading 'a_1 & ... & a_n impl*y* c' might be mistaken to mean that each a_i on its own implied c. * 2.3.4 Object and Data Property Expression Axioms - There is exactly one axiom 'about both object and data property expressions', namely a key constraint. Why not call it by this name in this section? - Right-hand part of the table: This big formula is difficult to navigate through. Is this version perhaps a bit more handy? forall x, y, u_1, ..., u_m, v_1, ..., v_n: ISNAMED(x) and ISNAMED (y) and for all i=1,...,m (ISNAMED(u_i)) and x in (CE)^C and for all i=1,...,m ( in (OPE_i)^OP) and for all j=1,...,n ( in (DPE_j)^DP) and y in (CE)^C and for all i=1,...,m ( in (OPE_i)^OP) and for all j=1,...,n ( in (DPE_j)^DP) implies x=y. - This one is even shorter: forall x, y, u_1, ..., u_m, v_1, ..., v_n: ISNAMED(x) and ISNAMED (y) and for all i=1,...,m (ISNAMED(u_i)) and x,y in (CE)^C and for all i=1,...,m ( in (OPE_i)^OP and in (OPE_i)^OP) and for all j=1,...,n ( in (DPE_i)^DP and in (DPE_i)^DP) implies x=y. * 2.3.6 Ontologies - Why Int' and not Int? Up to here, Int' hasn't been defined. - When do we say "an ontology O" (above) and when "an OWL 2 ontology O" (below)? * 2.4 Models - According to Section 2.2, .^I only operates on *named* individuals, hence Int' coincides with Int? - Given that this document will be released in a form similar to the existing one, it's quite difficult to tell .^{I'} from .^I . * 3 Independence of the Semantics from the Datatype Map - Theorem 1: "N_{DT}" followed by the comma looks rather like "N_{DT'}". - Theorem 1, maps in D': Shouldn't the dash (prime) be included in the superscripts? Anyway, all the small dots might not be readable clearly enough. This, of course, is rather a reason against including the dash into the superscript, but the way it's currently written it looks strange. - Theorem 1: Entailment *w.r.t. a datatype* hasn't been defined. The same for interpretation *w.r.t. a datatype* (in the proof), if I haven't overlooked it. - First sentence of the proof: The use of "contrapositive" here is somewhat misleading: The statement of the theorem is an implication a => b, whose consequent b is an equivalence b_1 <=> b_2. At first sight, it reads as if you want to prove ~b <=> ~a, but in fact you are proving a => (~b_1 <=> ~b_2). - Proof, third-last sentence ("Clearly, ComplementOf(DT)^DT subset ComplementOf(DT)DT'"): The map .^DT' hasn't ben defined because Int' uses .^DT. Furthermore, why is it enough to consider only data range expressions of the form ComplementOf(DT) and not ComplementOf(DR) for arbitrary DR, or DatatypeRestriction(DT, ...)? - This section might be more intuitive for non-experts if the last paragraph appeared before the proof.