Hi all,

Executive summary: The text of [1] is a little unintelligible, and
does not quite match what the SROIQ paper [2] says. At the very least,
it is not clear whether some of the bulleted lists are conjunctions or
disjunctions without very careful reading.

The definition of 'regular' order doesn't seem to be standard (at
least, I've not come across it) so perhaps it should be defined in the
OWL spec rather than deferring to the reference [2].

I spent a good few minutes puzzling about the seemingly circular
definition of simplicity before I moved on to the regularity
definition (which breaks the cycle). Perhaps regularity should be
defined before simplicity for the sake of other readers?

I think the translation of the definition of regularity from [2] into
the language of OWL should read as:

[[
... each axiom in Ax of the form SubObjectPropertyOf(SUB PE) in Ax
fulfils at least one of following conditions:

  * SUB is of the form SubObjectPropertyChain(PE PE)
  * SUB is of the form InverseObjectProperty(PE) and
  * SUB = SPE where SPE < PE
  * SUB = SubObjectPropertyChain(SPE1 ... SPEn) where n >= 2 and 
        SPEi < PE for 1 <= i <= n
  * SUB = SubObjectPropertyChain(PE SPE1 ... SPEn) where n >= 1 and
        SPEi < PE for 1 <= i <= n
  * SUB = SubObjectPropertyChain(SPE1 ... SPEn PE) where n >= 1 and
        SPEi < PE for 1 <= i <= n
]]

(NB I'm assuming that conditions 3, 4, and 5 of [2] permit n = 1; if
they also permit n = 0 then add 
[[
  * SUB = PE
]]
to the list -- it's not clear whether they do or not but this would
seem like a reasonable (trivial) extension)

Now to the definition of simple. The SROIQ paper only talks about role
*names* on the RHS of an inclusion, not inverted roles, and seems to
delete double-inversions, so this doesn't quite match up with OWL's
syntax. I'm going to be conservative about this until I get a chance
to sit down with pencil and paper and check a more liberal approach.

If OPU is an objectPropertyURI then it is not clear to me whether 
    SubObjectPropertyOf(InverseObjectProperty(OPU) OPU)
permits OPU to be simple - I suspect it does, although I don't think
this is implied by the conditions in [2]. Also the trivial axiom
    SubObjectPropertyOf(OPU OPU)
should not break the simplicity of OPU, either. If my reading is
right:

[[
An objectPropertyExpression InverseObjectProperty(OPE) is simple if
(OPE) is.

An objectPropertyURI OPU is simple if both of the following conditions
hold:

* For all axioms in Ax of the form
    SubObjectPropertyOf(SUB InverseObjectProperty^n(OPU)) (n >= 0),
SUB is a single objectPropertyExpression (not a
SubObjectPropertyChain) which is either simple or of the form
InverseObjectProperty^m(OPU) for some m >= 0. If Ax has no axiom of
the form 
    SubObjectPropertyOf(SUB InverseObjectProperty^n(OPU)) (n >= 0),
then OPU is simple. 

* Ax contains no axiom of the form 
    TransitiveObjectProperty(InverseObjectProperty^n(OPU))
]]

Finally, the constraint on the use of non-simple OPEs is clear enough,
except a little nomenclature has changed since it was written.

[[
    * ObjectMinCardinality, ObjectMaxCardinality,
        ObjectExactCardinality, and ObjectExistsSelf descriptions,
    * FunctionalObjectProperty and InverseFunctionalObjectProperty
        axioms, and
    * IrreflexiveObjectProperty, AsymmetricObjectProperty and
        DisjointObjectProperties axioms.
]]

The two bullet-points of axioms is a little confusing; the first are
cardinality constraints in disguise and the second are from role
assertions rather than the role hierarchy, but this distinction is
unimportant for the spec so it might be better to concatenate them.

Finally, there's something a little troubling about not having a
wellfoundedness constraint on the role hierarchy, which means that
checking for simplicity could not be decidable.

Phew.

Cheers,

Dave



[1] http://www.w3.org/Submission/2006/SUBM-owl11-owl_specification-20061219/#7
[2] http://www.cs.man.ac.uk/%7Esattler/publications/sroiq-tr.pdf

--
Dave Turner  Cube T400, HP Labs Bristol, Filton Road, Bristol BS34 8QZ
davidt@hp.com          +44 117 3129104 (Work) +44 7962 811627 (Mobile)