HermiT entailments that contain negation

Question

Is there a way to get inferences from HermiT reasoner that contain negation (ObjectComplementOf)? Here is what I tried:

OWLOntologyManager manager = OWLManager.createOWLOntologyManager();
dataFactory = manager.getOWLDataFactory();
IRI iri = IRI.create("http://www.test.owl");
OWLOntology ontology = manager.createOntology(iri);

OWLClass clsA = dataFactory.getOWLClass(IRI.create(iri + "#A"));
OWLClass clsB = dataFactory.getOWLClass(IRI.create(iri + "#B"));
OWLAxiom axiom = dataFactory.getOWLSubClassOfAxiom(clsA, clsB.getComplementNNF());

OWLIndividual john = dataFactory.getOWLNamedIndividual(IRI.create(iri + "#JOHN"));
OWLClassAssertionAxiom assertionAxiom = dataFactory.getOWLClassAssertionAxiom(clsA, john);

ontology.add(axiom);
ontology.add(assertionAxiom);

OWLReasonerFactory reasoner_factory = new ReasonerFactory();
OWLReasoner reasoner = reasoner_factory.createReasoner(ontology);

OWLOntology inferred_ontology = manager.createOntology();

// Create an inferred axiom generator, and add the generators of choice.
List<InferredAxiomGenerator<? extends OWLAxiom>> gens = new ArrayList<>();
gens.add(new InferredSubClassAxiomGenerator());
gens.add(new InferredClassAssertionAxiomGenerator());
gens.add(new InferredDisjointClassesAxiomGenerator());
gens.add(new InferredEquivalentClassAxiomGenerator());

// Create the inferred ontology generator, and fill the empty ontology.
InferredOntologyGenerator iog = new InferredOntologyGenerator(reasoner, gens);
iog.fillOntology(dataFactory, inferred_ontology);

The (cleaned) result:

//KB:   A SubClassOf not(B), A(JOHN)
ENTAILMENTS:{
    SubClassOf(A owl:Thing),
    SubClassOf(B owl:Thing),
    DisjointClasses(A owl:Nothing),
    DisjointClasses(B owl:Nothing),
    DisjointClasses(A B),
    ClassAssertion(owl:Thing JOHN),
    ClassAssertion(A JOHN)
}

My question: How can I also get this assertion: ClassAssertion(ObjectComplementOf(B) JOHN)?

Answer 1

It's not possible to generate all inferred axioms that use class or property expressions. The reason for that is that the list of class (and property) expressions is infinite, so the reasoner would embark on an impossible task if it tried to generate all axioms of that kind.

If you have a criterion for selecting a finite subset of class expressions (e.g., the list of complements for each named class in the ontology) you could implement an axiom generator that asks the reasoner whether those classes have instances, and create the axioms that way.

Reasoners could also do the same, to provide a partial answer to a question with infinite answers - but, far as I'm aware, there are no reasoners which do that. HermiT certainly does not.