CODEWITHSUNDEEP
owlprotegedescription-logicpellet
Median Hilal
Median Hilal

Reputation: 1531

Inferring that two object properties are equal in OWL

Given an ontology O, and let A, B two classes and object properties P and Q such that:

  1. P domain A
  2. P range B
  3. A ⊑ =1 P.⊤
  4. Q ⊑ P
  5. A ⊑ =1 Q.⊤

Thus, we to prove P ≡ Q, we only need show that P ⊑ Q, because we already have the other direction, Q ⊑ P, in (4). To conclude that P ≡ Q are equivalent; let

  1. (x,y) ∈ P

then x ∈ A and y ∈ B and we have from (5) that Q relates each individual of A to exactly one individual of B; then there must exist y′ ∈ B such that (x,y′) ∈ Q; and by (4), we can infer that

  1. (x,y′) ∈ P

Then, from (3), (6), and (7), we can infer that y = y′. Thus, if (x,y) ∈ P, then (x,y) ∈ Q, which means that:

  1. P ⊑ Q

Then, by (4) and (8):

  1. P ≡ Q

Questions:

  1. Is this conclusion true?
  2. Reasoners (e.g., Pellet, via the Protégé plugin) are not inferring P ≡ Q, however each time I assert P(a,b), the reasoner infers Q(a,b), and vice versa!

Upvotes: 1

Views: 672

Answers (1)

Dmitry Tsarkov
Dmitry Tsarkov

Reputation: 768

Your reasoning is correct and P is indeed equivalent to P1 in this ontology. However, Pellet, as the most of current DL reasoners, do not perform inferences on the property hierarchy. It is calculated as a reflexive transitive closure of the told information of property hierarchy relation. To the best of my knowledge the only reasoner that perform complete property hierarchy calculation is HermiT; if you classify your ontology with it then the inference P EquivalentTo P1 will appear in the inferred object property hierarchy view.

Upvotes: 2

Related Questions