Search code examples
owlsemantic-webprotegepellet

OWL: inverse of a property

Let's say we have four properties : 

ObjectProperty: superProp1 
       InverseOf: superProp3   

ObjectProperty: prop1  
      InverseOf: prop2       
      SubPropertyOf:superProp1   

ObjectProperty: prop2  
      InverseOf: prop1   

ObjectProperty: superProp3

Pellet deduces that prop2 is a subproperty of superProp3.
I can't understand this result.

Solution

  • Assuming :a :prop2 :b, one can infer that :a :superProp3 :b (for any :a and :b):

    1. Let's suppose that :a :prop2 :b.

    2. Then :b :prop1 :a holds, because :prop2 is an inverse of :prop1.

    3. Then :b :superProp1 :a holds, because :prop1 is a subproperty of :superProp1.

    4. Then :a :superProp3 :b holds, because :superProp1 is an inverse of :superProp3.

    Slightly more formally:

    T1.  :a :prop1 :b <=> :b prop2 :a              #  :prop1 owl:inverseOf :prop2  
T2.  :a :prop1 :b => :a :superProp1 :b         #  :prop1 rdfs:subPropertyOf :superProp1
T3.  :a :superProp1 :b <=> :b :superProp3 :a   #  :superProp1 owl:inverseOf :superProp3

A1.  :a :prop2 :b                              #  assumption, eliminated by T4
A2.  :b :prop1 :a                              #  A1, T1, modus ponens
A3.  :b :superProp1 :a                         #  A2, T2, modus ponens
A4.  :a :superProp3 :b                         #  A3, T3, modus ponens

T4.  :a :prop2 :b => :a :superProp3 :b         #  A1, A4, deduction theorem; QED

    More info: