Consequence-Based Reasoning: PTIME Classification

📍 Where we are: Part III · The EL Completion Algorithm — Chapter 11. Soundness and Completeness proved the six rules a trustworthy decision procedure; now we name the style of reasoning they embody, and see why it — and not tableau search — is what buys EL its polynomial-time classification.

We built the completion algorithm, watched it saturate two tables, and proved it sound and complete. What we never stepped back to notice is that it belongs to a whole family of reasoners, distinguished from the mainstream by one refusal: it never guesses. It never assumes a conclusion is false to see what breaks; it never opens a branch and backtracks. It just grinds facts forward until nothing new appears. That refusal has a name, consequence-based reasoning, and it is not a stylistic quirk — it is the single design decision that turns classification from a potentially exponential search into a guaranteed polynomial-time computation.

The simple version

Imagine two detectives on the same case. The first works by contradiction: she assumes the suspect is innocent, chases down every branching alibi, and backtracks the moment a story collapses — if every possible innocent story ends in a contradiction, guilt is proven. The second never entertains a hypothesis at all. She pins to a board only the facts the evidence forces, then the facts those force, and keeps sweeping the board until a full pass adds not a single new card. Whatever is pinned when the board stops growing is the truth. EL reasoning is the second detective — and this chapter is the story of why she never has to guess, and why that makes her fast.

What this chapter covers

• Two paradigms, contrasted — model-building by refutation (the tableau method, with case splits and backtracking) versus consequence-based saturation (forward, monotone, no backtracking), laid side by side in a trade-off table.
• Why EL has no case splits — dropping disjunction removes every "try this or that" choice, so a single monotone pass to a fixpoint suffices; that is the exact source of the polynomial-time bound.
• The completion operator is a $T_P$ — the saturation loop is an immediate-consequence operator over subsumption atoms, its least fixpoint the classification, the identical shape as Volume 1's forward chaining.
• Reading the trace as waves — the academic world's saturation $(23,0) \to (34,7) \to (39,7) \to (39,7)$, read as the closure filling in pass by pass, and the fixpoint detected the instant a full pass adds nothing.
• Why it scales — consequence-based classification is precisely what lets ELK classify SNOMED CT; a foreshadowing of the reasoners chapter.
• The unsolved part — EL is Horn, so one saturation suffices; beyond Horn, consequence-based methods must reintroduce a clever, controlled form of splitting, and the same forward-saturation idea, applied to rules instead of subsumptions, is Datalog — the door into Part IV.

Two ways to decide a subsumption

The job of a classifier is to decide entailment: does the TBox $\mathcal{T}$ force $A \sqsubseteq B$, written $\mathcal{T} \models A \sqsubseteq B$, meaning every interpretation that obeys the axioms also puts every $A$ inside $B$? There are two fundamentally different algorithmic strategies for answering that question, and telling them apart is the whole point of this chapter.

The first is model-building by refutation, the strategy behind the classical tableau method. To decide $\mathcal{T} \models A \sqsubseteq B$, it assumes the goal is false — it posits an individual that is an $A$ but not a $B$ — and then tries to build a complete, consistent model of $\mathcal{T}$ containing that individual. If every attempt to finish the model collapses into a contradiction (a clash, deriving $\bot$), then no such individual can exist, and the subsumption holds. The engine of this method is search, and the search branches because of disjunction. An axiom of the form $X \sqsubseteq Y \sqcup Z$ ("$\sqcup$" is or) forces a choice: the model-builder must try making the individual a $Y$, and if that whole branch clashes, backtrack and try $Z$ instead. Each disjunction multiplies the branches, and in the worst case the tree of choices is exponentially large. The oracle we trusted in the previous chapter, HermiT, is exactly such a reasoner — a hypertableau calculus over the full SROIQ logic behind OWL 2 DL — and its power to decide that enormous logic is bought precisely with that branching search.

The second strategy is consequence-based reasoning [1]. It never posits a countermodel and never branches. It starts from the axioms as asserted consequences and repeatedly applies inference rules that only ever add entailed consequences — subsumptions and role edges that genuinely follow — until a full sweep of the rules adds nothing. The answer is then read straight off the closure: $A \sqsubseteq B$ holds exactly when $B$ landed in $S(A)$. There is no hypothesis to refute, no branch to open, no state to discard on backtracking. This is precisely what the completion algorithm of the last two chapters was doing; we simply had not named the paradigm.

aspect	model-building / refutation (tableau)	consequence-based (saturation)
core move	assume the goal false, try to build a countermodel	assume nothing, derive entailed consequences forward
nondeterminism	case splits on disjunction, with backtracking	none — one monotone pass, no backtracking
state	build and discard candidate models	grow one saturated set, never discard
read the answer	no model exists ⟹ entailed	$B \in S(A)$ ⟹ entailed
best fit	expressive DLs with $\sqcup$, $\neg$ (ALC, SROIQ)	Horn DLs without $\sqcup$ (EL, EL++)
worst-case cost	exponential search tree	polynomial saturation (EL: cubic)
exemplar	HermiT (hypertableau)	ELK, CEL (completion)

Two answers to the same question: the tableau method branches and backtracks through a search tree that can grow exponentially, while consequence-based saturation climbs one monotone staircase to a fixpoint — and the reason EL can use the cheap right-hand method is that it has no disjunction to branch on. Original diagram by the authors, created with AI assistance.

The source of PTIME: no disjunction, no case splits

Why can EL get away with the cheap strategy when full OWL 2 DL cannot? The answer is a single missing constructor. The EL family keeps exactly conjunction $\sqcap$ and existential restriction $\exists r.C$; it has no disjunction $\sqcup$ and no negation $\neg$ (the one flavour of "no" it allows is the bottom concept $\bot$, handled by a single non-branching rule). Every axiom therefore has a forced consequence, never a chosen one. When CR3 sees $\text{Professor} \sqsubseteq \exists\text{advises}.\text{Student}$, there is exactly one edge to add; there is never a moment where the reasoner must weigh "make it a $Y$ or make it a $Z$" and prepare to undo the wrong guess. Remove the only source of branching and the search tree collapses to a single trunk — one monotone pass, repeated to a fixpoint.

This is not a soft observation; it is the whole complexity story. In logical terms EL is a Horn description logic: its axioms translate into Horn clauses, whose heads carry no disjunction, and that is exactly the condition Volume 1 identified as making the immediate-consequence operator monotone. Recall the load-bearing warning from Fixpoints: $T_P$ is monotone because rule bodies are positive conjunctions — adding a fact can only satisfy more rules, never fewer — and "had a body contained a negation … growing the fact set could switch that condition off and destroy a previously-derivable head, breaking monotonicity and with it every guarantee above." Disjunction breaks it the mirror way: a disjunctive conclusion is not a single fact to add but a choice among facts, and choices demand search. EL is engineered to contain neither, so its consequence operator stays monotone and its closure stays deterministic.

The payoff is a hard complexity separation. Adding disjunction and negation to get ALC makes concept satisfiability with respect to a general TBox ExpTime-complete — provably exponential in the worst case. EL subsumption, by contrast, is decidable in time polynomial in the size of the TBox, in fact cubic $O(n^3)$, and this PTIME bound is the headline result that the completion algorithm delivers [2]. Same question — does $A \sqsubseteq B$ follow? — but the language you pose it in decides whether the honest algorithm searches or merely saturates.

The completion operator is a $T_P$ over subsumption atoms

Once you see completion as consequence-based, its kinship with Volume 1 stops being an analogy and becomes an identity. Forward chaining took a set of ground atoms and applied the immediate-consequence operator $T_P$ — "fire every rule whose body holds, add the heads" — climbing from the base facts to the least fixpoint that is the meaning of the program. Completion does the identical thing, only its "atoms" are subsumption facts. Bundle one full pass of the six rules CR1–CR4, the bottom rule, and the role-chain rule into a single operator $T$ acting on the state $X = (S, R)$:

$$T(S, R) \;=\; (S, R)\ \text{enlarged by one simultaneous firing of every completion rule.}$$

Because no rule ever deletes an entry — each only calls S[A].add(...) or add_r(...) — the operator is monotone: a larger state can only yield a larger state, $X \subseteq X' \Rightarrow T(X) \subseteq T(X')$. That is the one property Knaster–Tarski and the Kleene climb of Volume 1 require, so the classification is nothing but the least fixpoint reached from the seed state $X_0 = \big(\{A \mapsto \{A, \top\}\},\ \varnothing\big)$:

$$\mathrm{lfp}(T) \;=\; \bigcup_{k \ge 0} T^k(X_0), \qquad A \sqsubseteq B \iff B \in S(A)\ \text{at}\ \mathrm{lfp}(T).$$

The companion file states this identity in its own docstring, in as many words (el_completion.py lines 32–33):

    The whole thing is just a **fixpoint of a monotone operator** — the very same
    shape as the forward-chaining T_P of Volume 1, now over subsumption facts.

So the four constructions Volume 1 promised would keep returning — forward chaining, Datalog evaluation, transitive closure, and description-logic completion — are here revealed as one construction wearing a fourth mask. The subsumer ledger $S$ is the fact set; the completion rules are the program $P$; $T$ is $T_P$; and classification is $\mathrm{lfp}(T_P)$. Everything you proved once about the climb transfers wholesale.

Reading the saturation as a wave of consequences

Because it is a Kleene climb, we can watch it climb. The complete function instruments each pass, recording the total sizes of $S$ and $R$ after every round so a reader can see the consequences spread (el_completion.py lines 205–213):

    def sizes():
        s = sum(len(v) for v in S.values())
        r = sum(len(v) for v in R.values())
        return s, r

    rounds = [sizes()]
    changed = True
    while changed:
        changed = False

The exit test while changed is the fixpoint condition $T(X) = X$ made executable: changed stays False for an entire pass exactly when no rule can add anything, which is exactly when the state maps to itself. Running the module on the academic world prints the climb — the real, committed output of python3 el_completion.py:

saturation reached a fixpoint in 3 rounds
  round : |S| |R|  (derived subsumers, derived role pairs)
      0 :  23   0
      1 :  34   7
      2 :  39   7
      3 :  39   7

Read the two columns as two ascending chains climbing in lockstep, the direct twin of Volume 1's [23, 41, 47, 47] fact-count waves. Each wave records what one application of $T$ newly settles, so watching the sizes climb is watching the closure fill in pass by pass:

round	$\lvert S\rvert$	$\lvert R\rvert$	new subsumers	new edges	what this wave is
0	23	0	—	—	the seed: each concept knows only itself and ⊤
1	34	7	+11	+7	one busy pass — CR1–CR⊥ cascade: the hierarchy, all 7 role edges, both unsatisfiable concepts caught
2	39	7	+5	+0	CR1 lifts Researcher ⊑ Person onto the five subclasses that gained Researcher in round 1
3	39	7	+0	+0	frontier stops advancing — the fixpoint, certified

Round 1 is a single busy pass, and because the rules always fire in the same order — CR1, then CR2, CR3, CR4, the bottom rule, and the role chain — a whole chain of dependent inferences can settle inside it. CR1 installs the asserted hierarchy; CR3 lays down all 7 role edges at once; CR4 then re-derives Researcher through those fresh advises edges (the axiom $\exists\text{advises}.\top \sqsubseteq \text{Researcher}$ firing on edges CR3 just made) — a cross-check of the direct Professor ⊑ Researcher axiom, and the only route by which TenuredStudentAdvisor earns Researcher; CR2 catches TenuredStudent holding both Professor and Student and stamps it $\bot$; and the bottom rule immediately crawls that $\bot$ backward along advises to condemn TenuredStudentAdvisor. Every one of the 11 new subsumers and all 7 edges is a round-1 consequence. Round 2 adds exactly five subsumers and no edges, and all five are the same fact — Person — from a single rule: CR1 on the axiom Researcher ⊑ Person. That axiom could only fire in round 1 for the concepts that already held Researcher when its turn in the pass came, which was just Researcher itself. The other five — Professor, Student, Dean, TenuredStudent, TenuredStudentAdvisor — gained their Researcher elsewhere in round 1, too late for that pass's CR1 to lift it, so their Person lands one wave behind, exactly as person(alice) waited a wave behind researcher(alice) in Volume 1. Round 3 fires everything once more, adds nothing ($39 = 39$, $7 = 7$), and that idle pass is the engine proving to itself that it is finished. Notice what this does not say: the round counter bounds the number of passes, not proof depth. Because a single pass can cascade several dependent firings — TenuredStudentAdvisor's $\bot$ alone rode CR1 → CR2 → CR3 → the bottom rule inside round 1 — a wave is an upper bound on the consequences newly settled, not a count of inference hops. A deeper ontology would take more passes, but the number of passes stays polynomially bounded because the ledgers themselves cannot grow past a polynomial ceiling.

Why consequence-based reasoning scales

The trade-off table's last two rows are where this paradigm stops being a toy and starts running biomedicine. Because there is no search tree, the total work is proportional to the size of the closure — the number of entries the rules can ever add — and EL guarantees that closure stays polynomial: with $n$ concept names, $S$ holds at most $n^2$ subsumer entries and each $R(r)$ at most $n^2$ pairs, so a monotone loop that adds at least one entry per productive pass must halt in polynomially many passes. No amount of adversarial modelling can make an EL classification blow up exponentially, because there is no exponential object anywhere in the algorithm to blow up.

That guarantee is exactly what the reasoner ELK cashes in [3]. ELK is a consequence-based classifier built on these very completion rules, and it classifies SNOMED CT — a clinical ontology with hundreds of thousands of concepts — in seconds, because saturation parallelizes beautifully: different concepts' subsumer sets can be grown concurrently, since the rules only ever add and never conflict. A tableau reasoner, forced to search for a countermodel of an ontology that large, would drown; a consequence-based one merely climbs a taller staircase. This is the practical reason the OWL 2 EL profile exists at all, and it is the through-line into the reasoners chapter ahead, where ELK, CEL, and their kin are studied as production systems rather than textbook loops.

The unsolved part

The honest boundary is the very feature that made everything above work: EL is Horn, so a single monotone saturation suffices. The instant you step outside Horn — the moment an ontology contains a genuine disjunction, "every gene is coding or non-coding" — the clean picture cracks. A purely forward, no-backtracking pass can no longer be complete, because a disjunctive consequence is not one fact to add but a branching obligation, and completeness needs the reasoner to consider both branches. The open engineering question is how much of the no-backtracking speed can be kept while admitting just enough case-splitting to stay complete. The consequence-based paradigm has been pushed beyond Horn precisely by deriving disjunctive consequences and splitting only when an inference truly forces a choice, rather than eagerly branching on every disjunction the way a naive tableau does [1] — a hybrid that recovers much of saturation's efficiency for far more expressive logics, but whose worst case is once again exponential. Where exactly the affordable frontier lies is still an active research boundary, not a settled line.

There is also a second thread leaving this chapter, hiding in plain sight. Strip away the description-logic vocabulary and what remains — seed a set of facts, fire monotone rules that only add, saturate to a least fixpoint — is a general-purpose engine that does not care whether its facts are subsumptions or arbitrary relations. Applied to user-written rules over ground data, that same engine is Datalog: the immediate-consequence operator $T_P$ from Volume 1, now given a query language and an industrial runtime. Consequence-based classification and Datalog evaluation are two applications of one idea, which is exactly why the next part can reuse everything you have just learned.

Why it matters

For neuro-symbolic AI, the lesson of this chapter is that how a symbolic reasoner computes is as consequential as what it computes. A consequence-based reasoner is not merely correct; it is correct by construction in one forward direction, which is the same direction a differentiable reasoning layer runs. When Volume 4 replaces the crisp "is $B$ in $S(A)$?" with a soft score and iterates a smooth, monotone update to convergence, it is imitating precisely this saturation — a forward climb to a fixpoint, never a backtracking search. The paradigms that hybridize most naturally with learning are the forward, monotone, search-free ones, because a fixpoint can be differentiated through but a backtracking search tree cannot. Consequence-based reasoning is thus not just the reason EL is fast; it is the reason EL-style reasoning is the most neural-friendly shape a symbolic reasoner can take, and the crisp target any learned approximation of ontology reasoning must be measured against.

Key terms

• Consequence-based reasoning — deciding entailment by deriving entailed consequences forward until a saturation (fixpoint), with no hypothesis to refute and no backtracking; the paradigm the completion algorithm belongs to.
• Model-building / refutation (tableau) — the contrasting paradigm: assume the goal false, search for a countermodel, and report entailment when every branch clashes; branches on disjunction and can cost exponential time.
• Case split / backtracking — the nondeterministic choice a disjunction $\sqcup$ forces on a model-builder, and the undoing of a failed choice; absent from EL because EL has no disjunction.
• Horn description logic — a DL (like EL) whose axioms are disjunction-free, so its immediate-consequence operator is monotone and a single saturation is complete.
• Immediate-consequence operator $T$ / $T_P$ — one simultaneous firing of all completion rules on the state $(S, R)$; monotone, and classification is its least fixpoint $\mathrm{lfp}(T)$.
• Saturation wave — the growth of $\lvert S\rvert$ and $\lvert R\rvert$ in one round (one application of $T$); an upper bound on the consequences newly settled that pass rather than a proof-depth counter, since the fixed intra-pass rule ordering can collapse several dependent firings into a single wave, and an idle wave certifies the fixpoint.
• PTIME classification — EL subsumption decided in polynomial (cubic) time, the guarantee that consequence-based saturation delivers and tableau search cannot.
• ELK — a consequence-based EL reasoner that classifies SNOMED CT's hundreds of thousands of classes in seconds by parallelizing rule firing.

Where this leads

We have now seen the completion algorithm from every angle: as an engine (the six rules and the while changed loop), as a certified decision procedure (sound, complete, terminating), and finally as an instance of a general paradigm (consequence-based, monotone, PTIME). The thread that closes this part is the observation that the paradigm is bigger than description logic. The next chapter, Datalog, takes the very same forward-saturation engine — the $T_P$ operator climbing to a least fixpoint — and turns it into a general rule language over ground data, with a query interface and a runtime engineered to make the climb fast at scale. The completion algorithm classified an ontology; Datalog will let you write your own rules and saturate them the same way, opening Part IV, where reasoning stops being about concept hierarchies and becomes about arbitrary relations.