- From: Jie Bao <baojie@gmail.com>
- Date: Mon, 4 Oct 2010 19:04:37 -0400
- To: Pavel Klinov <pklinov@cs.man.ac.uk>
- Cc: Cristian Cocos <cristi@ieee.org>, public-owl-dev <public-owl-dev@w3.org>
Yes, I believe Markus' solution will work As to using universal role on lhs of property inclusion, I copied from [1] the "Restriction on the Property Hierarchy". In our case, my understanding is that one such partial order exists: {pCat, owl:topObjectProperty, pHuman} < love . From the definition of →*, it seems that we do not require love < owl:topObjectProperty even if SubObjectPropertyOf(love owl:topObjectProperty) is always true. I may be wrong. Jie =========== The relation → is the smallest relation on AllOPE(Ax) for which the following conditions hold (A → B means that → holds for A and B): * if Ax contains an axiom SubObjectPropertyOf( OPE1 OPE2 ), then OPE1 → OPE2 holds; and * if Ax contains an axiom EquivalentObjectProperties( OPE1 OPE2 ), then OPE1 → OPE2 and OPE2 → OPE1 hold; and * if Ax contains an axiom InverseObjectProperties( OPE1 OPE2 ), then OPE1 → INV(OPE2) and INV(OPE2) → OPE1 hold; and * if Ax contains an axiom SymmetricObjectProperty(OPE), then OPE → INV(OPE) holds; and * if OPE1 → OPE2 holds, then INV(OPE1) → INV(OPE2) holds as well. The property hierarchy relation →* is the reflexive-transitive closure of →. Restriction on the Property Hierarchy. A strict partial order (i.e., an irreflexive and transitive relation) < on AllOPE(Ax) exists that fulfills the following conditions: * OP1 < OP2 if and only if INV(OP1) < OP2 for all object properties OP1 and OP2 occurring in AllOPE(Ax). * If OPE1 < OPE2 holds, then OPE2 →* OPE1 does not hold; * Each axiom in Ax of the form SubObjectPropertyOf( ObjectPropertyChain( OPE1 ... OPEn ) OPE ) with n ≥ 2 fulfills the following conditions: o OPE is equal to owl:topObjectProperty, or o n = 2 and OPE1 = OPE2 = OPE, or o OPEi < OPE for each 1 ≤ i ≤ n, or o OPE1 = OPE and OPEi < OPE for each 2 ≤ i ≤ n, or o OPEn = OPE and OPEi < OPE for each 1 ≤ i ≤ n-1. [1] http://www.w3.org/TR/owl2-syntax/#The_Restrictions_on_the_Axiom_Closure On Mon, Oct 4, 2010 at 18:06, Pavel Klinov <pklinov@cs.man.ac.uk> wrote: > Try Markus' solution, I'm quite sure it will work. > > Others will correct me if I'm wrong, but I think that the universal > role isn't allowed to appear on the left hand side of a chain (it > breaks the so called regularity conditions which are required for > decidability). > > Cheers, > Pavel > > On Mon, Oct 4, 2010 at 7:41 PM, Cristian Cocos <cristi@ieee.org> wrote: >>> Jie's below explanation shows a workaround that can be used for OWL 2. >>> This indirect encoding may not work well in practice, since tools for >>> modelling and reasoning will not recognise that you only want to make a >>> very simple statement when using the below axioms. >> >> I tried implementing Jie's suggestion and, surely enough, Pellet slapped me >> with an "UnsupportedFeatureException: Unsupported axiom: Ignoring >> transitivity and/or complex subproperty axioms for love" error message. Is >> this why you think this type of encoding may not work well? Why is it that >> Pellet and the other reasoners I tried balk at this? By the looks of it, >> your suggestion might not either, would it? >> >> Thanks, >> >> C >> >>> There are other >>> possible encodings that may or may not work better in specific >>> situations. Here is one more: >>> >>> EquivalentClasses( :Human ObjectHasValue( :pHuman :anIndividual ) ) >>> EquivalentClasses( :Cat ObjectHasValue( :pCat :anIndividual ) ) >>> SubObjectPropertyOf( ObjectPropertyChain( >>> :pHuman >>> ObjectInverseOf ( :pCat ) >>> ) :love) >>> >>> Here :pCat, :pHuman, and :anIndividual are auxiliary entities not used >>> anywhere else. Manchester Syntax would be something like this: >>> >>> ObjectProperty: love SubPropertyChain: pHuman o inv(pCat) >>> Class: Cat EquivalentTo: pCat value anIndividual >>> Class: Human EquivalentTo: pHuman value anIndividual >>> >>> Regards, >>> >>> Markus >>> >>> [1] http://korrekt.org/page/Elephants >>> (this is a special case of DL Rules; see my dissertation for an >>> extended >>> discussion: http://korrekt.org/page/PhD_thesis) >>> >>> >>> >>> On 01/10/2010 17:13, Jie Bao wrote: >>> > Cristian >>> > >>> > I guess you need a rule like Human(x),Cat(y) -> love(x,y) >>> > >>> > The trick is to use self restrictions, the top property and property >>> > chains to connect all x and y. >>> > >>> > in Functional-Style Syntax >>> > >>> > EquivalentClasses( Human ObjectHasSelf( ex:pHuman ) ) >>> > EquivalentClasses( Cat ObjectHasSelf( ex:pCat ) ) >>> > SubObjectPropertyOf( ObjectPropertyChain( ex:pHuman >>> owl:topObjectProperty >>> > ex:pCat ) ex:love) >>> > >>> > or in Manchester Syntax >>> > >>> > Class: Human EquivalentTo: ex:pHuman Self >>> > Class: Cat EquivalentTo: ex:pCat Self >>> > ObjectProperty: ex:love SubPropertyChain: ex:pHuman o >>> > owl:topObjectProperty o ex:pCat >>> > >>> > Wish that helps >>> > >>> > Jie >> >> >> > > > > -- > cheers, > --pavel > http://www.cs.man.ac.uk/~klinovp > >
Received on Monday, 4 October 2010 23:10:15 UTC