RE: Review OWL 2 MT Semantics Document

Hello Thomas,

Thank you very much for your detailed review comments -- I really appreciate them! I've been able to address most of them, apart
from some comments related to typesetting, which are difficult to address due to limitations of HTML. Please find below my
responses.

Here is the diff for the document:

http://www.w3.org/2007/OWL/wiki/index.php?title=Semantics&diff=12152&oldid=12103

Please let me know should you have further remarks about the way I've addressed your comments.

Thanks again for doing this!

Regards,

	Boris 

> -----Original Message-----
> From: Boris Motik [mailto:boris.motik@comlab.ox.ac.uk]
> Sent: 06 September 2008 17:40
> To: boris.motik@comlab.ox.ac.uk
> Subject: Review
> 
> =====================================================================
> 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.
> 

I've changed the sentence as follows:

The semantics given here is strongly related to the semantics of description logics [<cite>[[#ref-description-logics|Description
Logics]]</cite>] and is compatible with the semantics of the description logic ''SROIQ'' [<cite>[[#ref-sroiq|SROIQ]]</cite>].

>   - 5th sentence: *a* core part? And again, semantics equivalent to
>     the definition of a language?
> 

I've changed the sentence as follows:

Since OWL 2 is an extension of OWL DL, this document also provides a formal semantics for OWL Lite and OWL DL; this semantics is
equivalent to the official semantics of OWL Lite and OWL DL [<cite>[[#ref-owl-abstract-syntax-and-semantics|OWL Abstract Syntax and
Semantics]]</cite>].

>   - Apart from the two above comments, I find the
>     motivation/justification of the pursued approach strong and
>     helpful.
> 

Thanks!

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

All sets in the definition of the vocabulary are now called V_*. Thus, we now have N_DT in the datatype map and V_DT in the
vocabulary. I hope things are now clearer.

>   - Currently, this document contains 'data type' (e.g., in this
>     subsection) and 'datatype' (in the following subsection).
> 

I've changed this; thanks!

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

I appreciate this comment; however, I am not sure that there is a simple way of addressing it. The problem is that HTML is simply
not a good typesetting system for mathematics. I tried various versions of notation and neither seems ideal.

- Lowercase letters are often unreadable when typeset in italics (which I've used to typeset formulae through the specification).
This is particularly acute in superscripts. (Also, I've used capital letters for various parts of the syntax in all other documents
and changing all this would require quite a bit of work at this point and we would risk introducing errors.)

- One might call all interpretation functions IDT, IC, IOP, and so on. But then the individual interpretation function becomes II,
which looks strange.

- Using arbitrary letters for the interpretation functions is bad because the reader always needs to keep referring to their
definition.

- In LaTeX I would use \mathcal for the interpretation functions; unfortunately, there is no \mathcal in LaTeX. The best
approximation is bold, but then the document looks rather silly.

Capital letters are readable and they do not stick out that much (as bold letters do). I have therefore left the document as it is.
Please note that expressions such as (DT)^DT do not occur in many places in the 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.
> 

I thought it would be better to present all semantic conditions on Int in tables. (In standard DLs, \top and \bottom are class
expressions, and you usually define their semantics in tables anyway.) I agree, though, that this might confuse people, so I've
moved the semantic conditions on all built-in vocabulary up. Thus, the document now says, e.g., ".^c is a class interpretation
function such that [the conditions for owl:Thing and owl:Nothing are listed here]".

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

Agreed.

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

Agreed.

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

I've rephrased the paragraph to make these two points clear.

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

I've checked with Ian, and he thought that "imply" is OK here: the idea is that "condition 1 and condition 2 and ... condition n
together imply something".

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

Agreed. I've updated the Syntax and the XML Syntax documents to reflect this change.

>   - 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 (<x,u_i> in (OPE_i)^OP)
>                       and for all j=1,...,n (<x,v_j> in (DPE_j)^DP)
>       and y in (CE)^C and for all i=1,...,m (<y,u_i> in (OPE_i)^OP)
>                       and for all j=1,...,n (<y,v_j> 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 (<x,u_i> in (OPE_i)^OP and <y,u_i> in (OPE_i)^OP)
>       and for all j=1,...,n (<x,v_j> in (DPE_i)^DP and <y,v_j> in (DPE_i)^DP)
>     implies x=y.
> 

In private communication Peter has suggested an even shorter way of writing this condition.

> * 2.3.6 Ontologies
> 
>   - Why Int' and not Int? Up to here, Int' hasn't been defined.
> 

Copy-paste error; thanks!

>   - When do we say "an ontology O" (above) and when "an OWL 2 ontology
>     O" (below)?
> 

Sure, thanks!

> * 2.4 Models
> 
>   - According to Section 2.2, .^I only operates on *named*
>     individuals, hence Int' coincides with Int?
> 

This was a bug in Section 2.2: .^I must operate on all individuals.

>   - Given that this document will be released in a form similar to the
>     existing one, it's quite difficult to tell .^{I'} from .^I .
> 

I understand; however, I don't think we can du much about it. Calling the interpretation Int_1 doesn't help, since 1 is then
displayed as I, which, IMHO, looks even worse. Note also that subscripts in superscripts are not displayed nicely in HTML. Again,
these are the limitations of HTML as a typesetting system for mathematics. 

> * 3 Independence of the Semantics from the Datatype Map
> 
>   - Theorem 1: "N_{DT}" followed by the comma looks rather like
>     "N_{DT'}".
> 

I've split the sentence in hope that things are clearer this way; however, there is not much I can do given that we are in HTML.

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

I've moved the prime into the superscript.

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

The datatype map was implicit in the definition of Int and, therefore, it was implicit in the definition of all inference problems
as well. To make this clear, I have rewritten the definition of all inference problems accordingly.

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

I don't necessarily agree that the usage of "contrapositive" is ambiguous here; however, to make everybody happy, I've removed this
term from the proof.

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

D' should use .^{DT'}; this was a typo.

Regarding the second comment, you're right: one must consider other data ranges as well. I've corrected this by saying that O1 and
O2 are assumed to be in NNF and then generalizing the statement such that DR is a datatype, a datatype restriction, or an enumerated
data range.

>   - This section might be more intuitive for non-experts if the last
>     paragraph appeared before the proof.
> 
> 

Agreed. I've rephrased the paragraph slightly and have also added a remark about the fact that the datatype map does not need to be
listed explicitly when mentioning various reasoning problems.

Received on Saturday, 6 September 2008 19:05:37 UTC