hermitpy.Reasoner

Classification

Consistency is a search over the whole ontology. Class subsumption is a separate search that ignores the ABox. The direct hierarchy is built from those subsumption answers.

Consistency

is_consistent asks whether the loaded TBox and ABox together have a model. The first answer is cached. An empty graph is consistent and has no subclass pairs.

A class can be empty while the ontology stays consistent. Unicorn subclass of both Horse and NotHorse, with those two disjoint, is unsatisfiable, and the ontology still has a model: just do not use Unicorn.

Empty classes

unsatisfiable_classes returns the sorted named classes for which the atom is not satisfiable in the TBox. That test ignores the ABox. The fragment has no nominals, so a consistent ABox does not change class subsumption.

If is_consistent is false, every named class is returned. There is no model in which to separate them.

Direct pairs

direct_subclasses refuses an inconsistent ontology. It does not report every class as a subclass of owl:Nothing.

For a consistent ontology it tests subsumption between owl:Thing and each satisfiable named class. A is subsumed by B when A and not B is unsatisfiable in the TBox. A pair is direct when no third satisfiable class sits strictly between them. Every satisfiable class with no stricter named parent is paired with owl:Thing.

A chain Dog ⊆ Animal ⊆ Organism therefore yields three pairs: Dog–Animal, Animal–Organism, and Organism–Thing. Dog–Organism is omitted because Animal is between them.

Equivalents

If two satisfiable named classes subsume each other, both directions are returned: (Dog, Canine) and (Canine, Dog). Each of them is also linked to the same direct named parents. Neither is linked to owl:Thing when a stricter parent such as Animal exists.

Unsatisfiable classes

Each unsatisfiable named class is paired with owl:Nothing. Unsatisfiable classes are also reported as equivalent to each other, both directions. They are not placed under the satisfiable classes they were declared to subclass. Those declared parents are already implied by emptiness, and the hierarchy among satisfiable classes is computed separately.

Source: reasoner.py.