CODEWITHSUNDEEP
owlsemantic-webprotegepellet
alex
alex

Reputation: 7905

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.

Upvotes: 1

Views: 1093

Answers (2)

Stanislav Kralin
Stanislav Kralin

Reputation: 11479

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:

Upvotes: 2

Arthur Va&#239;sse
Arthur Va&#239;sse

Reputation: 1581

Maybe using less abstract naming can give you a feeling of what's going on. Lets consider the same problem described using words having a semantic.

We know the following rules : Being Wet is the inverse of being Dry. It exist another kind of wetness, ReallyWet. Being ReallyWet always imply you're Wet, thus it is a subproperty of Wet. Finally, we also know that being ReallyWet is the opposite of being ReallyDry.

From this you -and pellet- can then conclude that ReallyDry is a kind of dryness.

Why ? The reasoning is : Dry is the inverde of Wet ReallyDry is the inverse of ReallyWet ReallyWet is a subproperty of Wet -> ReallyDry is the inverse of a subproperty of Wet, and as such is should be the subproperty of the inverse of Wet. Conclusion : ReallyWet is a subproperty of Wet.

Does it sound logic ? I think that pellet can explain the rule it used to deduce some triples. It probably is : ( A inverse of B ) AND ( C inverse of D ) AND
(C is a sub property of A) -> D is a sub property of B

Upvotes: 1

Related Questions