RE: All humans love (all) cats

Mystery solved: in my ontology "love" (...as it were) was a subproperty of a property that had a disjoint declaration. Once I removed it, Pellet ran just fine. (It took me a lot of agonizing to realize that, and Pellet's error message didn't help either...)

Many thanks,

C

P.S. Before removing it it's easy to guess that Markus' workaround didn't work either...

> -----Original Message-----
> From: Jie Bao [mailto:baojie@gmail.com]
> Sent: Monday, October 04, 2010 20:05
> To: Pavel Klinov
> Cc: Cristian Cocos; public-owl-dev
> Subject: Re: All humans love (all) cats
> 
> 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

Cristian Cocos
Post Doctoral Fellow
Centre for Logic and Information, StFX University 54B St. Mary's Street, Antigonish NS, Canada B2G 2W5
Tel: + 1 (902) 867-4931, Fax: +1 (902) 867-1397

Current research: "Building Decision-Support Through Dynamic Workflow Systems for Health Care"

Received on Tuesday, 5 October 2010 15:20:59 UTC