Infer non-trivial OWL superclasses (or subclasses) assertions using a Java reasoner

Question

I want to express the following DL assertions in OWL

A ⊑ B
A ⊑ ∃R

meaning that A is subconcept of B and all the instances of A must have a relation R with something else.

I'm expressing it with the following OWL ontology:

Prefix(:=<http://example.org/my-ontology#>)

Ontology(<http://example.org/my-ontology>
    Declaration(Class(:A))
    Declaration(Class(:B))

    Declaration(ObjectProperty(:R))

    SubClassOf(:A :B)
    SubClassOf(:A ObjectSomeValuesFrom(:R owl:Thing))
)

I'm using the HermiT reasoner for retrieving all the super-classes of :A, in this way:

OWLOntology ontology = TestUtils.ontology;
OWLReasonerFactory reasonerFactory = new StructuralReasonerFactory();
ConsoleProgressMonitor progressMonitor = new ConsoleProgressMonitor();
OWLReasonerConfiguration config = new SimpleConfiguration(progressMonitor);
OWLReasoner reasoner = reasonerFactory.createReasoner(ontology, config);
reasoner.precomputeInferences();

for (OWLClass owlClass : ontology.getClassesInSignature()) {
    if (owlClass.toStringID().contains("#A")) {
        System.out.println("Class=>" + owlClass.toStringID() + "\nSuperClass[");
        System.out.println("\t" + reasoner.getSuperClasses(owlClass, false));
        System.out.println("]");
    }
}

but this is printing only:

Class=>http://example.org/my-ontology#A
SuperClass[
    Nodeset[Node( <http://example.org/my-ontology#B> ), Node( owl:Thing )]
]

How can I also get the information about SubClassOf(:A ObjectSomeValuesFrom(:R owl:Thing))?

P.S. I cannot just list the inclusion assertions from the ontology but I have to use a reasoner (not necessary HermiT) for possibly inferring them.

Answer 1

The inferences that follow from an ontology is infinite. See this paper for example.

For this reason reasoners usually limit inferences to named classes. \exists R is not a named class, hence it is not returned as an inference.

To get the required inference, you need to give \exists R a name by adding for example

C \equiv \exists R

The reasoner then will be able to infer A is a subclass of C.