

Review OWL 2 MT Semantics Document

From: Thomas Schneider <schneidt@cs.man.ac.uk>
Date: Wed, 3 Sep 2008 19:34:30 +0200
Message-Id: <FE94654C-4D1B-44C5-9D03-8A9757B8D7D7@cs.man.ac.uk>
To: public-owl-dev@w3.org, team-owl-chairs@w3.org
Review for "OWL 2 Web Ontology Language -- Model-Theoretic Semantics"
revision 12088:


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

  - 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

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

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

* 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

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

Hi all,

I've read and commented the Model-Theoretic Semantics document http://www.w3.org/2007/OWL/wiki/Semantics 
  ; please find attached a summary. I'm open for discussions.


|  Dr Thomas Schneider                             
schneider@cs.man.ac.uk |
|  School of Computer Science          http://www.cs.man.ac.uk/ 
~schneidt |
|  Kilburn Building, Room 2.114                    phone +44 161  
2756136 |
|  University of  
Manchester                                              |
|  Oxford Road                                               _/// 
_       |
|  Manchester M13 9PL                                         
(o~o)       |

Glentaggart (n.)
  A particular type of tartan hold-all, made exclusively under licence  
  British Airways.
  When waiting to collect your luggage from an airport conveyor belt,  
  will notice that on the next conveyor belt along there is always a
  single, solitary bag going round and round uncollected. This is a
  glentaggart, which has been placed there by the baggage-handling staff
  to take your mind off the fact that your own luggage will shortly be
  landing in Murmansk.

                     Douglas Adams, John Lloyd: The Deeper Meaning of  
Received on Thursday, 4 September 2008 07:20:12 GMT
