hermitpy

hermitpy.tableau

Tableau

Satisfiability is a search over a completion graph. Nodes carry concepts in negation normal form. Edges are role successors. A clash closes a branch. An open, complete graph is a model.

Two questions

Ontology consistency starts from the ABox. Each named individual is a root node, class assertions and literal assertions label that node, and object-property assertions are edges.

Concept satisfiability starts from one fresh root labeled with the concept, plus the TBox. It does not copy the ABox. Callers check is_consistent first when they need the ontology, not a class, to have a model.

An empty ABox uses the same one-node start as a concept test with no extra concept, which asks whether the TBox alone is consistent.

Rules

Each node is saturated before the search branches:

  1. Every general concept inclusion is added to the node.
  2. A conjunction adds each operand.
  3. A named class adds the concepts stored as its unfolding.
  4. A universal restriction copies its filler to each neighbor along that role. On a transitive role, the universal itself is copied to the neighbor as well.
  5. An edge adds the role's domain concepts to the source and its range concepts to the target.

owl:Thing is never stored. Adding a concept that is already on the node does nothing.

After saturation, an open disjunction is a choice point. The search tries each operand on a copy of the graph and stops at the first open branch. If every branch clashes, the concept is unsatisfiable.

Existential restrictions that are not yet witnessed create one successor and then saturate again. The successor is labeled with the filler, unless the filler is owl:Thing, in which case the edge alone is enough. Only one successor is created per pass.

Blocking

A node is blocked when an ancestor has the same label, that ancestor's parent has the same label as this node's parent, and both edges use the same role. A node under a blocked parent is blocked too. Blocked nodes do not spawn further successors. This pairwise check is what keeps inverses and transitive roles from building an infinite chain, as in a person who must have a person as a parent.

Datatype clashes

A node clashes when it contains owl:Nothing, or a named class and the negation of that same class. It also clashes when a datatype existential or an asserted literal cannot meet the universal restrictions on that property. Numeric bounds are intersected. A complemented range excludes its positive part. Distinct families, such as a number and a string, do not intersect, except that rdfs:Literal meets any family.

Bounds

The search refuses a graph of 256 nodes, and a branch deeper than 4096. Either case raises ReasonerLimitExceeded. Those bounds are safety stops for this fragment search. They are not a completeness proof for OWL beyond the fragment.

Source: tableau.py and syntax.py.