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