In OWL, is a sub-property of an irreflexive property also irreflexive? Likewise is a sub-property of an asymmetric property also asymmetric?
Logically, they should be, but I can't find anything in the OWL documentation that specifies that this is the case.
Consider the following example:
:parent-of a owl:IrreflexiveProperty .
:father-of a owl:ObjectProperty ;
owl:subPropertyOf :parent-of .
Based on this ontology, the following would not be allowed because parent-of is irreflexive:
_:max :parent-of _:max .
But is father-of implicitly irreflexive as well? In other words, would this also be prohibited:
_max :father-of _:max .
If you think of a property as a set of arrows which connect pairs of points, then irreflexive just means that there are no arrows which both start and end at the same point. A sub-property is simply a subset of those arrows, and so the sub-property of an irreflexive property is necessarily also irreflexive. Likewise with asymmetric properties. But again, I don't know if OWL spells this out explicitly or if OWL reasoners are supposed to make this "assumption".
In OWL, is a sub-property of an irreflexive property also irreflexive? Likewise is a sub-property of an asymmetric property also asymmetric?
Yes. The logical formulation is in OWL 2 Web Ontology Language Direct Semantics (Second Edition):
2.3.2 Object Property Expression Axioms
Satisfaction of OWL 2 object property expression axioms in I is defined as shown in Table 6.
…
- Axiom: IrreflexiveObjectProperty( OPE )
- Condition: ∀ x : x ∈ ΔI implies ( x , x ) ∉ (OPE)OP
Your reasoning shows that any subproperty of an irreflexive property satisfies the condtition. Therefore, the subproperty is also irreflexive.
But again, I don't know if OWL spells this out explicitly or if OWL reasoners are supposed to make this "assumption".
OWL reasoners are based on these definitions, and so should be able to infer that the subproperty is irreflexive.