Nonstructural Restrictions on Axioms (OWL/1.1 Syntax Section 7)

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)

Received on Friday, 9 March 2007 15:51:19 UTC