EL Reasoners: ELK and CEL

📍 Where we are: Part V · Reasoners in Practice — Chapter 15. Certain Answers read trustworthy answers off a chase by homomorphism, filtering out the null-witnessed tuples; now we leave the hand-built machinery and meet the reasoners that actually ship — ELK and CEL — which run our Part III completion algorithm at industrial scale, and we put our own from-scratch version on trial against one of them.

Part III proved six completion rules sound, complete, and terminating; Part IV pushed the same fixpoint machinery into Datalog and the chase. A fair question hangs over all of it: is any of this real? Does a deployed system genuinely classify an ontology by normalizing a TBox and saturating two tables to a fixpoint — or is that only the textbook's teaching story? This chapter answers plainly. Two shipping reasoners, ELK and CEL, are that completion algorithm, engineered for speed, and they classify medical vocabularies with hundreds of thousands of concepts in seconds. Because the companion cannot bundle ELK, it validates its from-scratch completion a different way: against HermiT, a reasoner of an entirely different kind, which agrees on every entry.

The simple version

Imagine you built, from a textbook, your own machine for sorting a library into its subject hierarchy — and it works flawlessly on a shelf of ten books. The real test is whether the same idea survives a national library of hundreds of thousands of volumes. ELK and CEL are that idea built for the national library: the very completion algorithm of Part III, tuned to classify a hospital's entire medical vocabulary in seconds. And since we cannot bundle their engine here, we check our own version a different way — we run it beside a completely different kind of reasoner, HermiT, and confirm the two agree on every single entry.

What this chapter covers

• From algorithm to product — ELK and CEL are real reasoners built on the completion / consequence-based method; CEL came first, for life-science ontologies, and both cash EL's deliberate poverty in for real-world speed.
• What makes an EL reasoner fast — rule indexing, concurrency, and tables that only ever grow: no backtracking, so classification is polynomial in the worst case and near-linear in practice.
• Where they run — SNOMED CT and the Gene Ontology, hundreds of thousands of concepts, classified routinely; the deployed case for the OWL 2 EL profile.
• The cross-check we can run — owlready2 ships HermiT, not ELK, so reasoners.py rebuilds the academic world and drives HermiT via sync_reasoner.
• The committed result — from-scratch 8 subsumptions, HermiT 8, both the same two unsatisfiable concepts, AGREEMENT CONFIRMED.
• Why HermiT is a fair oracle — it is complete for OWL 2 DL, whose logic is a strict superset of EL, so it would expose any bug in the from-scratch reasoner; ELK would give the identical EL classification.

From algorithm to product: ELK and CEL

Recall the shape of the algorithm in el_completion.py. Normalize every axiom into one of four normal forms — NF1: $A \sqsubseteq B$; NF2: $A_1 \sqcap A_2 \sqsubseteq B$; NF3: $A \sqsubseteq \exists r.B$; NF4: $\exists r.B \sqsubseteq A$ — then saturate two tables — $S(A)$, the concepts $A$ is known to be subsumed by, and $R(r)$, the pairs $(A, B)$ where $A$ is known to have an $r$-successor in $B$ — by firing rules until nothing changes, then read off $A \sqsubseteq B$ as "$B \in S(A)$." The module's own docstring names what that loop 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" (el_completion.py lines 32–33). That is not a toy pattern invented for teaching. It is the engine of two real reasoners.

CEL is the elder — a polynomial-time reasoner built specifically for life-science ontologies [1]. It was the first system to demonstrate that a specialized EL classifier could handle the terminologies that general-purpose reasoners of the day choked on. ELK — "the incredible ELK" — is the modern successor: a consequence-based reasoner for the OWL 2 EL profile (OWL is the Web Ontology Language), indexed and concurrent, engineered to classify SNOMED CT in seconds [2]. Both belong to the family Part III's consequence-based-reasoning chapter named: they derive consequences forward and saturate, never searching for a refutation. That is the sharp contrast with HermiT, which decides subsumption the opposite way — by trying to build a counter-model and backtracking whenever a branch clashes.

Reasoner	Logic it decides	Method	Where it shines
CEL	EL+ / EL++	consequence-based completion	first polynomial-time life-science classifier (SNOMED CT, Gene Ontology) [1]
ELK	OWL 2 EL	consequence-based, indexed and concurrent	classifies SNOMED CT in seconds [2]
HermiT	OWL 2 DL (SROIQ ⊇ EL)	hypertableau — model search with backtracking	complete oracle for the full logic [3]

Both EL reasoners buy their speed with the trade the EL family chapter set up: EL is deliberately poor. It keeps only conjunction ⊓ and the existential restriction ∃, and gives up universal restriction ∀, negation ¬, and disjunction ⊔. That poverty is exactly what makes subsumption decidable in polynomial time — and ELK and CEL are the systems that cash the guarantee.

Two reasoning cultures over one ontology: the consequence-based EL family (CEL, ELK) grows S and R monotonically to a fixpoint and scales to SNOMED CT, while HermiT searches for a model and backtracks — yet on the academic world both land on the same 8 subsumptions and the same 2 unsatisfiable concepts. Original diagram by the authors, created with AI assistance.

What makes an EL reasoner fast

Three engineering facts, all visible in the from-scratch code, explain why ELK and CEL are quick.

The tables only ever grow, so there is no backtracking. Saturation builds an ascending chain of derived-fact sets that never shrinks,

$$D_0 \;\subseteq\; D_1 \;\subseteq\; D_2 \;\subseteq\; \cdots \;\subseteq\; D_k \;=\; D_{k+1},$$

capped by the finite universe of possible $(A, B)$ facts, so it must stabilize. Every addition is guarded to count only when it is genuinely new — the helper that records a role edge returns True only when the pair was absent (el_completion.py lines 198–203):

    def add_r(r, pair):
        R.setdefault(r, set())
        if pair not in R[r]:
            R[r].add(pair)
            return True
        return False

Nothing is ever retracted, so there is no wrong guess to undo. That is the defining difference from a tableau reasoner like HermiT, which posits an individual, propagates, hits a clash, and backtracks to try another branch. A consequence-based EL reasoner has no branches: it grinds monotonically to one fixpoint.

Rule indexing — each rule scans only what it can fire on. Before the loop runs, the axioms are bucketed by shape, so a rule matching normal form NF4 ($\exists r.B \sqsubseteq A$) never even looks at an NF1 axiom ($A \sqsubseteq B$) (el_completion.py lines 191–196):

    nf1 = [a for a in normalized if a[0] == "nf1"]
    nf2 = [a for a in normalized if a[0] == "nf2"]
    nf3 = [a for a in normalized if a[0] == "nf3"]
    nf4 = [a for a in normalized if a[0] == "nf4"]
    chains = [a for a in normalized if a[0] == "chain"]
    rsubs = [a for a in normalized if a[0] == "rsub"]

Ours is the toy version; ELK does the same at industrial strength, indexing millions of axioms so each inference consults only the handful that can possibly fire [2].

Concurrency. The saturation of each concept is a largely separable unit — its derived role successors are communicated between units rather than every unit re-deriving the whole — and ELK exploits exactly this to partition the work across cores and classify large ontologies in parallel [2].

The worst-case cost is bounded the way the soundness and completeness chapter established. Writing $N$ for the concept names and $N_R$ for the roles,

$$\sum_{A} |S(A)| \;\le\; |N|^2, \qquad \sum_{r} |R(r)| \;\le\; |N_R| \cdot |N|^2,$$

so the two tables can only grow to a polynomial size, and the saturation therefore halts after polynomially many productive passes — the PTIME (polynomial-time) guarantee. On real ontologies the completed relation stays sparse, and ELK's measured behavior is near-linear in the input size [2].

Where they run: SNOMED CT and the Gene Ontology

The reason the OWL 2 EL profile exists at all is a deployment. SNOMED CT (the Systematized Nomenclature of Medicine, Clinical Terms) has hundreds of thousands of clinical concepts, and it is authored in a fragment close to OWL 2 EL precisely so that a reasoner like ELK or CEL can classify the entire thing in seconds. The Gene Ontology is the same story on the biology side. This is the deployed case for OWL 2 EL: the profile was standardized around what these consequence-based classifiers can do at scale, not the reverse [2][1].

And the modelling-bug check the bottom rule performs is exactly the check these reasoners run on real terminologies. When a class is accidentally made a subclass of two disjoint classes, it lights up as unsatisfiable — the same failure the deliberately over-constrained TenuredStudent triggers when it is declared both a Professor and a Student under $\text{Professor} \sqcap \text{Student} \sqsubseteq \bot$. And TenuredStudentAdvisor is dragged down with it: because it must advise a TenuredStudent — itself now ⊥ — the bottom rule propagates ⊥ back along the advises edge, so it too is flagged unsatisfiable. On a vocabulary of hundreds of thousands of concepts, that is a curator's smoke alarm: the reasoner names the offending class instead of silently classifying a contradiction.

The cross-check we can actually run

We cannot ship ELK inside a pure-Python companion, so the validation uses the reasoner owlready2 does bundle. As reasoners.py explains, "owlready2 bundles HermiT (a complete OWL 2 DL reasoner) and Pellet; it does not ship the EL-specialised ELK, so we drive HermiT via sync_reasoner — a strict superset of EL, so agreement here is the strongest possible check" (reasoners.py lines 11–13). The module rebuilds the identical academic-world ontology — 10 named concepts, 6 roles, 14 TBox axioms — axiom for axiom in owlready2's Python syntax (reasoners.py lines 45–51):

    world = get_ontology("http://nesy-guide.org/academic.owl")
    with world:
        # Concept names (declared so the hierarchy is explicit).
        class Person(Thing): pass
        class Researcher(Person): pass          # (3) Researcher ⊑ Person
        class Professor(Researcher): pass       # (1) Professor ⊑ Researcher
        class Student(Researcher): pass         # (2) Student ⊑ Researcher

The two harder EL++ axioms — disjointness and the role chain — map onto owlready2 constructs one-for-one (reasoners.py lines 72–75):

        # (6) Professor ⊓ Student ⊑ ⊥  (disjointness)
        AllDisjoint([Professor, Student])
        # (7) advises ∘ advises ⊑ grandAdvisor
        grandAdvisor.property_chain.append(PropertyChain([advises, advises]))

Then reasoner_classification runs HermiT and reads off exactly the two things the from-scratch code reports — subsumptions and unsatisfiable concepts among the named concepts — filtered the same way, so the two answers are directly comparable (reasoners.py lines 98–103):

    with world:
        sync_reasoner(world, infer_property_values=False, debug=0)

    named = set(onto.CONCEPTS)
    unsat = {c.name for c in world.inconsistent_classes()
             if c.name in named}

The committed result: agreement confirmed

Run it, and the two independent code paths — one built straight from the textbook rules, one a decade-hardened engine — land on the identical classification. This is the real committed output of python3 reasoners.py:

Reasoner (HermiT via owlready2) vs. from-scratch EL completion
  from-scratch subsumptions : 8
  HermiT subsumptions       : 8
  from-scratch unsatisfiable: ['TenuredStudent', 'TenuredStudentAdvisor']
  HermiT unsatisfiable      : ['TenuredStudent', 'TenuredStudentAdvisor']

  subsumptions agree : True
  unsatisfiable agree: True

  AGREEMENT CONFIRMED — the from-scratch reasoner matches HermiT.

The 8 subsumptions are not a bare count; they are a concrete hierarchy the from-scratch reasoner prints on its own (python3 el_completion.py):

classification: 8 subsumptions between named concepts
  Dean ⊑ Person
  Dean ⊑ Professor
  Dean ⊑ Researcher
  Professor ⊑ Person
  Professor ⊑ Researcher
  Researcher ⊑ Person
  Student ⊑ Person
  Student ⊑ Researcher

unsatisfiable concepts (2): ['TenuredStudent', 'TenuredStudentAdvisor']

Every one of those eight — the three Dean subsumptions, the two Professor subsumptions, Researcher ⊑ Person, and the two Student subsumptions — is confirmed by HermiT, and both engines flag the same two unsatisfiable concepts. The assertion that enforces this refuses any drift: it compares the two result sets outright and would print their symmetric difference on a mismatch (reasoners.py lines 150–151):

    assert subs_agree, ("subsumption mismatch", r_subs ^ el_subs)
    assert unsat_agree, ("unsat mismatch", r_unsat ^ el_unsat)

It never fires. Two engines, two methods, one classification.

Why HermiT is a fair oracle

Agreement is only as strong as the witness, and HermiT is the strongest available here. It is a complete OWL 2 DL reasoner [3]: its decision procedure — a hypertableau calculus — is built for the full SROIQ description logic behind OWL 2 DL, a strict superset of the tiny EL fragment the completion algorithm handles. Two consequences follow.

First, HermiT is not a second copy of our own idea that might share the same blind spot. It decides subsumption by a completely different method — searching for a model rather than deriving consequences — over a far larger logic, so any bug in the from-scratch reasoner would surface as a disagreement, and none does. When an implementation and an independent, more powerful reasoner concur on every entry, the residual chance that both are wrong in the same way is about as small as external validation gets.

Second, ELK is redundant to the correctness question precisely because it would give the identical EL classification: it decides the same EL fragment by the same consequence-based method our code imitates. Checking against the heavier, more general HermiT is therefore deliberate — a superset oracle agreeing is stronger evidence than a same-fragment tool agreeing, because the superset oracle could in principle have found more than EL sees and instead found exactly the same. This is what the companion's chapter map records for soundness-completeness: "matches HermiT (8 subs, 2 unsat)."

The unsolved part

EL reasoners are specialists, and their speed is inseparable from their narrowness. The moment an ontology needs something outside EL — a universal restriction ∀r.C, a negation ¬C, a disjunction ⊔, or genuine cardinality — ELK and CEL simply cannot decide it. You must either fall back to a full-DL reasoner such as HermiT or Konclude and pay the worst-case blow-up of full-DL reasoning (SROIQ subsumption is 2NEXPTIME-complete), or hand the Datalog-shaped part to a rule engine such as RDFox. No single engine is best for every knowledge base, and the profile boundary — "is this axiom still EL?" — is today largely drawn by hand. The honest open question is whether a system could route each query automatically to the cheapest engine that can decide it: EL-fast where EL suffices, full-DL only where an axiom genuinely demands it, without a human first partitioning the ontology by profile.

A related caution applies to the cross-check itself. Agreement on the academic world corroborates the implementation on one input; it does not, and cannot, certify agreement on SNOMED CT. That universal guarantee is what the soundness-and-completeness theorem provides — the empirical handshake only confirms that this code faithfully realizes the theorem on one ontology, not that it would on every ontology. Testing shows the presence of agreement, never its guarantee; the proof is what closes that gap.

Why it matters

For neuro-symbolic AI, ELK is the existence proof that answers the standing objection that "logic does not scale." A reasoner that classifies hundreds of thousands of medical concepts in seconds — by nothing more exotic than saturating a monotone operator to its least fixpoint — shows that exact symbolic reasoning can be fast enough to sit inside a real system, not merely a proof on paper. That exact, sound-and-complete classification is the ground truth a learned or neural approximation must be measured against: when a later differentiable reasoner ranks subsumptions by plausibility, the 8 exact subsumptions and 2 exact unsatisfiabilities certified here are what say whether it drifted. And the two-engine handshake is a template the whole field reuses — when a fast specialist and a general oracle concur, you can trust the specialist and pay only its cheaper price.

Key terms

• ELK — a consequence-based reasoner for the OWL 2 EL profile; indexed and concurrent, it classifies SNOMED CT-scale ontologies in seconds by saturating the completion tables to a fixpoint.
• CEL — ELK's predecessor, the first polynomial-time reasoner built for life-science ontologies; same consequence-based method.
• Consequence-based reasoning — deriving consequences forward and saturating a monotone operator to a fixpoint, with no backtracking; the method behind ELK, CEL, and the from-scratch completion.
• OWL 2 EL — the tractable OWL profile (only ⊓ and ∃, plus ⊥, role chains) whose polynomial-time classification ELK and CEL implement; the deployed case for SNOMED CT and the Gene Ontology.
• HermiT — a complete OWL 2 DL reasoner over SROIQ (a strict superset of EL), deciding subsumption by hypertableau model search; used here as an independent oracle.
• Superset oracle — a reasoner for a larger logic used as an external witness; its agreement is stronger evidence than a same-fragment tool's, because it shares no method or blind spot with the code under test.
• Monotone saturation / no backtracking — the tables $S$ and $R$ only ever grow to a least fixpoint, so an EL reasoner never guesses and never undoes, which is why classification is near-linear in practice.

Where this leads

We now know the completion algorithm is not merely provably correct but deployed: ELK and CEL run it at SNOMED CT scale, and the from-scratch version matches a superset oracle entry for entry. But EL reasoners are specialists, and a general knowledge base needs more — rule engines for the Datalog-shaped part, full-DL reasoners for the axioms that leave EL behind. The next chapter, Datalog and DL Engines: RDFox, HermiT, Konclude, surveys those engines and closes a loop this volume has been circling since Part III: EL completion re-expressed as Datalog, so the specialist reasoner and the general rule engine turn out to be running one and the same fixpoint.