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
>>> >
>>> > Wish that helps
>>> >
>>> > Jie
>>
>>
>>
>
>
>
> --
> cheers,
> --pavel
> http://www.cs.man.ac.uk/~klinovp
>
>

Received on Monday, 4 October 2010 23:10:15 UTC