Re: Review OWL 2 MT Semantics Document

Hi Boris,

thanks very much for your response and the changes you've made. I  
agree with most of them, but have comments about the following ones:

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

I think it's a good idea to change the N_* to V_*. However, now the  
vocabulary V *over D* is not related to D any more: the enumeration of  
the V_* should at least contain the statements V_{DT} = N_{DT}, V_{LT}  
= N_{LT}, and V_{FA} = N_{FA}, shouldn't it?

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

I see.

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

Well, if it were just for this problem, then you could dispose of  
italics and make them upright. (These symbols are operator names, and  
those are usually typeset upright.)

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

Hm, I see ... this requires a careful trade-off between readibility  
and effort spent. Your judgement here is more reliable than mine,  
since I'm too new to the OWL WG documents.

I agree that the alternatives you listed aren't feasible.

> Please note that expressions such as (DT)^DT do not occur in many  
> places in the document.

Well .. but usually the first occurrence of a stumbling block is the  
worst; the others can then be anticipated ... ;-)

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

This is how I had it in mind. I find it clearer for this document (but  
would do it "as usual for DLs" in a conference or journal paper, too).
>
>> * 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.
>>
> I've rephrased the paragraph to make these two points clear.
>>

OK, I find it clearer now. However, I now have the same problem as  
Michael: my Firefox 3 shows the "alpha" as an italicised "a", while  
Firefox 2 showed a clear "alpha". How about turning the "alpha" into  
an "x" here?

>> ["imply" or "implies"]
>
> 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".

OK, sorry, I'll keep this in mind. ;-)

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

Thanks, but I'm not 100% satisfied with the new heading "Keys":  
Strictly speaking, "KeyFor(PE_1, ..., PE_n, CE)" is a key  
*constraint*. A key is an n-tuple of individuals filling the  
properties PE_1, ..., PE_n. Being picky, I'd rather like to see the  
heading "Key Constraints" here ...

>> [Semantics of key constraints]
>
> In private communication Peter has suggested an even shorter way of  
> writing this condition.

Good, much clearer! I just feel that it should be made clearer that  
the antecedent of the "imply" is everything behind the colon. I know  
that this property doesn't make sense otherwise, but an extra pair of  
brackets or so might help the reader to grasp the structure of this  
non-trivial statement.

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

Thanks, that's better for understanding the statement of the theorem  
(but for the price of making the definitions of the inference problems  
slightly more lengthy).

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

Well, this was my mistake: I overlooked the fact that .^{DT'} was  
given in D'. Now there's Michael's comment that .^{C'} isn't defined.

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

I find this much clearer now.

Cheers

Thomas

+ 
------------------------------------------------------------------------+
|  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)       |
+-------------------------------------------------------oOOO--(_)-- 
OOOo--+

Glentaggart (n.)
  A particular type of tartan hold-all, made exclusively under licence  
for
  British Airways.
  When waiting to collect your luggage from an airport conveyor belt,  
you
  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  
Liff

Received on Sunday, 7 September 2008 12:42:38 UTC