From: Turner, David <davidt@hp.com>

Date: Fri, 9 Mar 2007 16:07:00 -0000

Message-ID: <86FE9B2B91ADD04095335314BE6906E8D6D4B3@sdcexc04.emea.cpqcorp.net>

To: <public-owl-dev@w3.org>

Received on Friday, 9 March 2007 16:07:14 GMT

Date: Fri, 9 Mar 2007 16:07:00 -0000

Message-ID: <86FE9B2B91ADD04095335314BE6906E8D6D4B3@sdcexc04.emea.cpqcorp.net>

To: <public-owl-dev@w3.org>

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

- text/plain attachment: OWL-1.1 Nonstructural Restrictions on Axioms.txt

*
This archive was generated by hypermail 2.3.1
: Wednesday, 27 March 2013 09:32:54 GMT
*