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

From: Turner, David <davidt@hp.com>
Date: Fri, 9 Mar 2007 15:51:09 -0000
To: <public-owl-dev@w3.org>
```
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

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

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 20:58:14 UTC