SuperProperty Of Chaining

Question

Imagine that given the following two relations:
a(x,y)
b(y,z)
we could derive that:
c(x,z)
then this can be explicitly expressed in Protégé by adding a SuperProperty Of (Chain) for the c property like this:
a o b SubPropertyOf c

With that expressed, imagine that we only know:
a(x,y)
c(x,z)
how can we explicitly express that we therefore also know:
b(y,z)
and this would again be with a SuperProperty Of (Chain), but for the b property?

I first thought to try:
a o inverse(c) SubPropertyOf b

This Protégé didn't like, saying there was a circle. Now I'm just very confused.

Answer 1

The correct expression for the b(y,z) would be inverse(a) o c SubPropertyOf b, as you want to express that the property path from y to z corresponds to b. If you have only this axiom this should give you necessary inference. However, you could not use it together with the first axiom, a o b SubPropertyOf c. In this case, you 'define' c via b in the axiom with direct properties and the b via c in the axiom with inverse property. So you have to know c to define c. This kind of loops are disallowed in OWL 2 DL, that's why Protege tells you about cyclical definitions. All in all, you can only have one of these axioms, but not both of them at the same time.

Answer 2

Knowing a and c does not entail b. That can be easily ilustarted with the classical example, definition of uncle:

:hasUncle
  rdf:type owl:ObjectProperty ;
  owl:propertyChainAxiom (
      :hasParent
      :hasBrother
    ) .

Then if :David :hasParent :Mary and :Mary :hasBrother :John, a DL reasoner would indeed infer that :David :hasUncle :John. But if we assert that :David :hasUncle :John and :David :hasParent :Mary, that is not sufficient to infer that :Mary :hasBrother :John. And indeed John can be a brother of another parent of Mary.

Please note that the definition statement says that the property chain is subProperty of :hasUncle and not equivalent property. So, even if you assert :hasParent as functional, the reasoner would still not infer b from a and c. However, OWL2 does not allow to have equivalent combination of object properties.

The property chains should be applied with care. For example, in S1 º S2 º S3 º ... º Sn ⊑ R, R can only be on the first or last place of the left side of the expression. Otherwise it won't be decidable. This is one of the restrictions to Regular RBoxes. And property chains, or more formally "General Role Inclusion" can only be decidable if applied to Regular RBoxes.