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

Argh, excuse the random line breaks. The most important one to correct
is

> [1]
http://www.w3.org/Submission/2006/SUBM-owl11-owl_specification-20061219/
#7

-- the fragment id is important! Grumble grumble Outlook grumble
grumble. Complete unmangled text attached.

Cheers,

Dave

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

> -----Original Message-----
> From: public-owl-dev-request@w3.org 
> [mailto:public-owl-dev-request@w3.org] On Behalf Of Turner, David
> Sent: 09 March 2007 15:51
> To: public-owl-dev@w3.org
> Subject: 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)
> 
>