Self-restriction in Protégé reasoner

Question

As an exercise on using self-restrictions, I have implemented a simple ontology in Protégé. The ontology contains the following things:

• object properties: REL, REL1 and REL2;
• individuals: x;
• Axioms:

  • x REL1 x

  • x REL2 x

  • REL1 o REL2 subPropertyOf: REL

  • REL some Self SubClassOf owl:Nothing

I expected the ontology to be inconsistent (indeed, "x REL1 x" and "x REL2 x" imply that "x REL x" which, in turn, implies that x is a member of the class "REL some Self"); however, when I run the reasoner (HermiT 1.4.3.456) no error is displayed. It seems that the reasoner ignores the axiom "REL some Self SubClassOf owl:Nothing".

The main part of my ontology (OWL Functional Syntax) is reported below:

Declaration(ObjectProperty(:REL))
Declaration(ObjectProperty(:REL1))
Declaration(ObjectProperty(:REL2))
Declaration(NamedIndividual(:x))

############################
#   Named Individuals
############################

# Individual: :x (:x)

ClassAssertion(owl:Thing :x)
ObjectPropertyAssertion(:REL1 :x :x)
ObjectPropertyAssertion(:REL2 :x :x)


SubClassOf(ObjectHasSelf(:REL) owl:Nothing)
SubObjectPropertyOf(ObjectPropertyChain(:REL1 :REL2) :REL)

Answer 1

TL;DR: This is cannot be reasoned on using OWL DL.

The longer explanation.

There are 2 reasons for this:

1. Reasoning is only in terms of known classes. I.e. the class REL Self is an anonymous class and in general inferences are not reported on anonymous classes. This is because if anonymous classes are considered, there are an infinite amount of explanations.

2. To fix issue 1 you can introduce a class to represent REL Self.

   Declaration(Class(:RelSelf))
   EquivalentClasses(:RelSelf ObjectHasSelf(:REL))
   

When you run the reasoner on this, you will get an error stating that you have used a non-simple role in a self restriction from the reasoner. To ensure decidability, SROIQ, the DL underpinning OWL 2 limits the use of roles. This paper explains these restrictions in detail.

There are 2 papers that you can read wrt obtaining finite explanations and issues around reasoning wrt properties:

1. Extracting finite sets of entailments
2. Preventing, Detecting, and Revising Flaws in Object Property Expressions