The deterministic skeleton under the fuzz

Formal methods underneath

Open the Russian dolls under a modern AI coding tool and you eventually hit Tree-sitter: incremental, error-tolerant parsers built on Bernard Lang's 1974 Generalized LR algorithm and a formal grammar per language. The lesson is that the death of Chomsky's generative grammars under the axe of LLMs was announced prematurely: for code, the fuzzy model depends on old, exact, formal-language machinery to do the load-bearing work.

Oxid-DB is the same story one layer up. The LLM / Sensory side proposes axioms: fuzzy guesses like "is a chunk a subclass of, or part of, a document?" The EL^⊥ classifier is the deterministic, sound skeleton underneath that decides what actually follows, and what contradicts. It is the deterministic logical check against the fuzzier extraction process, done in-process, in Rust, inside the database.

LLMs did not kill formal grammars: for code, they depend on them. Oxid-DB is that story one layer up: the model guesses, the reasoner decides.

One reasoner, one algorithm

In the taxonomy of ontology reasoners, Oxid-DB belongs with the ELK / CEL / Snorocket / jcel family, profile reasoners for the EL description logic, not the HermiT / Pellet family that reason over full OWL 2 DL. That is a deliberate engineering choice, not a shortcoming.

EL^⊥ is the logic. ELK is a reasoner for that logic. OWL 2 EL is the W3C profile built on the same family. Oxid-DB's classifier is its ELK.

Why EL, not full DL

HermiT and Pellet reason over OWL 2 DL: union (⊔), universal (∀), negation (¬), cardinality, nominals, inverses. That expressiveness costs a tableau search that is worst-case ExpTime / N2ExpTime. Oxid-DB instead restricts its class language to exactly five shapes:

ClassExpr =  | Named       -- Beer, Person, Disease …  | Top         -- ⊤   (everything)  | Bottom      -- ⊥   (the empty class)  | And(A, B)   -- A ⊓ B  | Some(r, A)  -- ∃r.A

That is the EL^⊥ profile: conjunction (And), existential restriction (Some = ∃r.C), ⊤ and ⊥. No ⊔, ∀, ¬, cardinality or nominals. The payoff is the result Baader, Brandt & Lutz proved in 2005 and ELK exploits: classification is polynomial, computed by fixpoint rule-application instead of backtracking search.

What it computes

Mapping onto the standard reasoning tasks: three are fully shipped, one is partial, one is deferred. The engine is honest about which is which.

The one Named only row is the single genuine gap, covered in The honest scope below.

Step A: normalize the TBox

The algorithm is normalize, then run completion rules to a fixpoint. First every axiom is rewritten into one of four canonical shapes the rules know how to consume:

And(a, b) ⊑ c        -- conjunctiona         ⊑ ∃r.b     -- existential on the right∃r.b      ⊑ c        -- existential on the lefta         ⊑ ⊥        -- explicit unsatisfiability

The elegant move is how disjointness disappears into conjunction. There is no dedicated disjointness machinery at all:

-- every declared-disjoint pair (A, B) is stored-- as ONE ordinary axiom: A ⊓ B ⊑ ⊥ -- "these two classes can never overlap" now runs-- on the same machinery as any other conjunction,-- there is no separate disjointness engine.

Step B: seed the facts

A worklist is primed with the truths that hold before any inference runs. Everything after this point is derived from these seeds by the completion rules.

-- the worklist is seeded with axiomatic truthsC ⊑ C            -- reflexivityC ⊑ ⊤            -- top…               -- every asserted SubClassOf…               -- every explicit  C ⊑ ⊥…               -- every existential right-hand side

Step C: run five completion rules

Each rule takes known subsumptions and derives new ones. The engine processes one derived fact a ⊑ b at a time and fires only the rules that fact can trigger, until nothing new appears.

Step D: realize individuals

Once the class hierarchy is closed, build_result walks each individual's asserted classes and, using the finished subsumption closure, drops it into the extent of every superclass:

Heineken : Pilsner -- using the finished subsumption closure, the-- individual drops into the extent of every-- superclass at once: Heineken ∈ extent(Pilsner)Heineken ∈ extent(PaleLager)Heineken ∈ extent(Beer)Heineken ∈ extent(Alcohol)Heineken ∈ extent(⊤)

Then, for every disjoint pair, it intersects the two extents. Any individual landing in both is an ABox consistency violation: e.g. Whiskers : Cat and Whiskers : Plant with Cat ⊓ Plant ⊑ ⊥ is reported, not silently dropped.

Two different “bad” verdicts

The engine is careful about a distinction that is easy to gloss: a broken schema and a broken dataset are not the same failure, and both are returned as data rather than thrown as errors.

Incoherence ≠ inconsistency: a TBox with an unsatisfiable class still has a model, the class is simply empty. Both are computed; both come back as structured results.

Where it plugs in

There is exactly one algorithm, and every reasoning path in the engine routes to it:

The Sensory indexer leans on this directly: it asserts axioms (SubClassOf, chunk ClassAssertion) and calls /classify to materialize the transitive IS-A closure. The named-subclass reasoning is genuinely done live by the database.

The honest scope: three tiers

The boundaries fall into three buckets. Only the last is a real gap.