The EL Family: Small Logic, Big Ontologies

📍 Where we are: Part II · Description Logic — Chapter 5. Description Logic handed us the full grammar of concepts and roles, the split between a TBox of definitions and an ABox of facts, and a model-theoretic semantics that says exactly what an axiom means. Now we do something that sounds like a mistake: we throw most of that grammar away — and discover the leftover fragment is precisely the one that scales to the largest ontologies on Earth.

Description logic gives you a rich language for defining concepts: negation, disjunction, universal and existential restrictions, cardinalities. The trouble is that richness has a price paid in time — the more you can say, the harder a machine must work to decide what follows, and past a certain point the work explodes. The EL family takes the opposite bet. It keeps a deliberately tiny sublanguage, proves that the tiny language is enough for a huge class of real definitions, and cashes the restraint in as a reasoner that stays fast no matter how big the ontology grows. This chapter is about that bet and why it wins.

The simple version

Imagine you may describe anything in the world, but only with three moves: name a category ("Professor"), say "this and that at once" ("a professor who advises a student"), and say "related to some thing of a kind" ("advises some student"). You may never say "not," never say "either/or," never say "all of them." It feels crippling — until you notice that almost every definition in a medical dictionary ("a heart attack is a tissue death caused by some blocked artery") uses only those three moves, and that because you took the dangerous words away, a machine can check millions of such definitions against one another in an afternoon. The EL family is that three-move language, made exact.

What this chapter covers

• What EL keeps — only conjunction $\sqcap$, existential restriction $\exists r.C$, and the top concept $\top$; a plain-language decoder for each, and a pointed list of everything it refuses.
• What EL++ adds back — the bottom concept $\bot$ (hence disjointness), role inclusions $r \sqsubseteq s$ and role chains $r \circ s \sqsubseteq t$, nominals, and the ABox — every one of which appears in the academic world — laid out in an EL-versus-EL++ table.
• Why the poverty pays — subsumption in EL and EL++ is decidable in polynomial time, against ExpTime and worse for expressive logics; a completion algorithm we quote and run is the reason.
• The academic world, classified — classify() normalizes 14 axioms into 16 normal-form axioms, saturates to a fixpoint in 3 rounds, and reads off 8 named subsumptions plus 2 unsatisfiable concepts.
• The subtle interplay — how two role axioms re-derive Professor ⊑ Researcher through the roles, so the little language is quietly doing real inference.
• The payoff in the wild — SNOMED CT and the Gene Ontology, hundreds of thousands of concepts each, classified by EL reasoners in practice.

The three moves EL keeps — and everything it throws away

A description logic builds compound concepts from concept names (like Professor), role names (like advises), and a fixed set of constructors. EL — E for $\mathcal{E}$xistential restriction, L for the lightweight base language that supplies conjunction and top — keeps exactly three constructors [1]. Writing $A$ for a concept name, $r$ for a role, and $C, D$ for any concepts, its whole grammar is one line:

$$C, D \;::=\; \top \;\mid\; A \;\mid\; C \sqcap D \;\mid\; \exists r.C$$

The ::= reads "is built as," and the vertical bars separate the alternatives. Decoded move by move: $\top$ (top, read "everything") is the concept every individual belongs to; $A$ is a bare concept name; $C \sqcap D$ (conjunction, the $\sqcap$ read "and") is the things that are both a $C$ and a $D$; and $\exists r.C$ (existential restriction, read "$r$-related to some $C$") is the things that have at least one $r$-successor lying in $C$. That is the entire toolkit. The academic world's ontology.py builds concepts with only two helper constructors, And and Some, exactly matching $\sqcap$ and $\exists$ (ontology.py lines 53-61).

Now the pointed part — what EL will not let you write:

• No negation ¬$C$. You cannot say "not a professor."
• No disjunction $C \sqcup D$. You cannot say "a professor or a student."
• No universal restriction $\forall r.C$. You cannot say "advises only students."

Every one of those is a constructor a richer logic like $\mathcal{ALC}$ offers freely, and every one is a constructor that, as the next section shows, makes reasoning combinatorially harder. EL's thesis is that their absence is a feature: strip the language to the three monotone, positive moves and the deciding stays cheap.

What EL++ adds back

Pure EL is almost too poor — it cannot even state that two classes are incompatible. EL++ (spoken "EL plus plus") is the extension that adds genuinely useful constructors without leaving polynomial time [1]. Crucially, it does not add negation or disjunction back; it adds a carefully chosen handful whose reasoning stays tractable, and every one of them appears in the academic world. Here is the full comparison.

Constructor	Syntax	Reads as	In EL?	In EL++?	Where in the academic world
Top	$\top$	everything (owl:Thing)	yes	yes	implicit in every $S(A)$
Concept name	$A$	an atomic class	yes	yes	Person, Professor, Student, Dean, …
Conjunction	$C \sqcap D$	both a $C$ and a $D$	yes	yes	Professor ⊓ Student; Person ⊓ ∃authored.Paper
Existential	$\exists r.C$	$r$-related to some $C$	yes	yes	∃advises.Student; ∃advises.Professor
Bottom	$\bot$	the empty class (owl:Nothing)	no	yes	Professor ⊓ Student ⊑ ⊥ (disjointness)
Role inclusion	$r \sqsubseteq s$	every $r$-edge is an $s$-edge	no	yes	supported via RoleSub (the chain below is the axiom used)
Role chain	$r \circ s \sqsubseteq t$	$r$ then $s$ implies $t$	no	yes	advises ∘ advises ⊑ grandAdvisor
Nominal	$\{a\}$	the class of exactly individual $a$	no	yes	ABox individuals as singleton concepts
ABox	$A(a)$, $r(a,b)$	assertions about individuals	no	yes	13 concept + 18 role assertions

The single most consequential addition is $\bot$ (bottom, read "nothing"), the concept no individual can belong to. It is what lets EL++ express disjointness: to say professors and students never overlap you assert that their conjunction is empty,

$$\text{Professor} \sqcap \text{Student} \sqsubseteq \bot,$$

which ontology.py writes as Sub(And("Professor", "Student"), BOT) (ontology.py lines 142-143). Deriving $A \sqsubseteq \bot$ for any named $A$ is precisely how the reasoner reports that $A$ is unsatisfiable — that you have accidentally defined a class nothing could ever instantiate. The academic world plants two such traps on purpose (a TenuredStudent declared both a professor and a student, and a TenuredStudentAdvisor who advises one) so the bottom rule has to earn its keep.

EL++ also adds role inclusions $r \sqsubseteq s$ and role chains $r \circ s \sqsubseteq t$ (the $\circ$ read "then," or "composed with"), the machinery behind the academic world's signature axiom advises ∘ advises ⊑ grandAdvisor — advising the advisor of someone makes you their grand-advisor. Finally it admits nominals (singleton concepts $\{a\}$ naming one individual) and, with them, the whole ABox of assertions, turning a pure schema language into one that can reason about named data. All told, the ten named concepts, six roles, and fourteen TBox axioms of ontology.py sit squarely inside EL++, and its summary() prints the shape exactly:

10 named concepts, 6 roles, 14 TBox axioms; ABox: 13 concept assertions, 18 role assertions over 13 individuals.

EL keeps three constructors; EL++ adds four more — bottom, role inclusion, role chain, and nominals with the ABox — and pays for the restraint with polynomial-time classification that scales from the ten-concept academic world to the hundreds of thousands of classes in SNOMED CT and the Gene Ontology. Original diagram by the authors, created with AI assistance.

Why the restraint pays: polynomial time

Here is the reason a logician would voluntarily give up negation and disjunction. The central reasoning task is subsumption: given a TBox, decide whether one concept is necessarily contained in another, written $C \sqsubseteq D$ ("every $C$ is a $D$"). For the EL family this decision is PTIME — solvable in time bounded by a polynomial in the size of the TBox — whereas the moment you add the constructors EL left out, the cost climbs steeply [1]:

$$\text{subsumption in } \mathcal{EL}^{++} \in \mathrm{PTIME}, \qquad \text{in } \mathcal{ALC} \in \mathrm{ExpTime}, \qquad \text{in } \mathcal{SROIQ}\ (\text{OWL 2 DL}) \in \mathrm{N2ExpTime}.$$

The jump from PTIME to ExpTime (exponential time) is not a tuning detail; it is the difference between an ontology that classifies in seconds and one that may not classify at all before you lose patience. What buys EL its polynomial bound is a completion (or saturation) algorithm [2]: rather than search for a counter-model the way an expressive-DL tableau does, it starts from the stated axioms and repeatedly fires a small fixed set of derivation rules, adding entailed subsumption facts until a round adds nothing — a fixpoint of a monotone operator, the very same shape as Volume 1's forward-chaining $T_P$. First every concept-inclusion axiom is rewritten into one of exactly four normal forms, with basic concepts $A, A_1, A_2, B$ (a name, $\top$, or $\bot$) on the leaves; the two kinds of role axiom — a role inclusion $r \sqsubseteq s$ and a role chain $r \circ s \sqsubseteq t$ — are left as they stand (which is exactly why the by-form breakdown below still carries a chain entry, one the role-chain rule CRχ then processes directly):

Normal form	Shape	Reads as
NF1	$A \sqsubseteq B$	a name is under a name
NF2	$A_1 \sqcap A_2 \sqsubseteq B$	a conjunction is under a name
NF3	$A \sqsubseteq \exists r.B$	a name has an $r$-successor of a kind
NF4	$\exists r.B \sqsubseteq A$	having such a successor puts you under a name

The reasoner then maintains two tables — $S(A)$, the names known to subsume $A$, and $R(r)$, the pairs $(A, B)$ with $A$ known to satisfy $\exists r.B$ — and saturates them with six completion rules (el_completion.py lines 23-30). The rules are the whole engine, so they are worth reading once:

Rule	Precondition	Adds	Purpose
CR1	$A' \in S(A)$, $A' \sqsubseteq B$	$B$ to $S(A)$	follow a name inclusion
CR2	$A_1, A_2 \in S(A)$, $A_1 \sqcap A_2 \sqsubseteq B$	$B$ to $S(A)$	fire a conjunction axiom
CR3	$A' \in S(A)$, $A' \sqsubseteq \exists r.B$	$(A, B)$ to $R(r)$	create a role edge
CR4	$(A, B) \in R(r)$, $B' \in S(B)$, $\exists r.B' \sqsubseteq C$	$C$ to $S(A)$	fire a successor axiom
CR⊥	$(A, B) \in R(r)$, $\bot \in S(B)$	$\bot$ to $S(A)$	propagate unsatisfiability
CRχ	$(A, B) \in R(r)$, $(B, C) \in R(s)$, $r \circ s \sqsubseteq t$	$(A, C)$ to $R(t)$	fire a role chain

Because each rule only ever adds to $S$ and $R$, and both are bounded by the number of concept names squared, the loop is monotone and must halt after polynomially many additions — the tractability guarantee made concrete.

Classifying the academic world

The public entry point ties the three movements — normalize, complete, classify — into one call. It is worth quoting in full (el_completion.py lines 302-319):

def classify(tbox=None, trace=False):
    """Normalize, complete, and return everything a classification report needs:
    a dict with the normalized axioms, fresh names, saturated S and R, the
    saturation ``rounds``, the ``subsumptions`` and the ``unsatisfiable`` set."""
    if tbox is None:
        tbox = onto.TBOX
    normalized, fresh = normalize(tbox)
    S, R, rounds = complete(normalized, trace=True)
    result = {
        "normalized": normalized,
        "fresh": fresh,
        "S": S,
        "R": R,
        "rounds": rounds,
        "subsumptions": subsumptions(S, only=set(onto.CONCEPTS)),
        "unsatisfiable": unsatisfiable(S),
    }
    return result if not trace else result

Running the module normalizes the 14 TBox axioms into 16 normal-form axioms (introducing two fresh names for the two compound axioms that were not already normal), then saturates $S$ and $R$ to a fixpoint. The trace shows the climb wave by wave — the derived-fact counts $|S|$ and $|R|$ rising and then standing still, exactly the "a round changes nothing" halt of a least fixpoint:

normalization: 14 axioms → 16 normal-form axioms, introducing 2 fresh names ['_N1', '_N2']
  by normal form: {'chain': 1, 'nf1': 6, 'nf2': 2, 'nf3': 3, 'nf4': 4}

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

The 'chain': 1 count is that role-chain axiom sitting untouched among the 16, while the remaining fifteen NF1–NF4 axioms (six NF1, two NF2, three NF3, four NF4) are what the four normal forms actually cover. Reading the answer off the saturated $S$ — $A \sqsubseteq B$ exactly when $B \in S(A)$ — yields the classification of the whole academic world in eight lines, plus the two deliberately broken concepts flagged unsatisfiable:

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 the eight is checkable by eye against the TBox. The stated hierarchy gives Professor ⊑ Researcher, Student ⊑ Researcher, Researcher ⊑ Person, and Dean ⊑ Professor directly; the reasoner's job is to compute their transitive closure, so that Professor ⊑ Person, Student ⊑ Person, Dean ⊑ Researcher, and Dean ⊑ Person all fall out even though no axiom states them. The two unsatisfiable concepts fail by different mechanisms. TenuredStudent, declared both a Professor and a Student, trips the disjointness axiom via CR2 alone: CR1 puts Professor and Student into $S(\text{TenuredStudent})$, and since $\text{Professor} \sqcap \text{Student} \sqsubseteq \bot$ is a single NF2 axiom whose right-hand side is $\bot$, CR2 fires on that pair and adds $\bot$ to $S(\text{TenuredStudent})$ directly — no role edge is involved. TenuredStudentAdvisor, whose only sin is to advise an (impossible) tenured student, is the one that needs CR⊥: the bottom rule propagates $\bot$ backward along the advises edge from the unsatisfiable successor to its predecessor. Two modelling bugs, caught for free by a polynomial-time reasoner — the everyday payoff of $\bot$.

The subtle interplay: roles re-deriving the hierarchy

It would be easy to dismiss EL as a glorified transitive-closure engine over a class tree. Two axioms in the academic world show it doing something a tree lookup never could: re-deriving a subsumption through the roles. Axiom (4) says every professor advises some student, and axiom (5) says anyone who advises anything at all is a researcher (ontology.py lines 132-138):

    # (4) Every professor advises some student.  Normal form A ⊑ ∃r.B.
    Sub("Professor", Some("advises", "Student")),

    # (5) Anyone who advises anything at all is a researcher.  Normal form ∃r.⊤ ⊑ A.
    # Together with (4) this *re-derives* Professor ⊑ Researcher through the roles,
    # a nice internal cross-check of the completion rules CR3 + CR4.
    Sub(Some("advises", TOP), "Researcher"),

Neither axiom mentions the other's concepts, yet together they entail Professor ⊑ Researcher — a fact the explicit hierarchy also states, arrived at by a completely independent route. Trace the two rules that do it (el_completion.py lines 227-238):

        # CR3: A' ∈ S(A), A' ⊑ ∃r.B  ⟹  (A, B) ∈ R(r)
        for _, a_prime, r, b in nf3:
            for A in names:
                if a_prime in S[A]:
                    if add_r(r, (A, b)):
                        changed = True

        # CR4: (A, B) ∈ R(r), B' ∈ S(B), ∃r.B' ⊑ C  ⟹  C ∈ S(A)
        for _, r, b_prime, c in nf4:
            for (A, B) in list(R.get(r, ())):
                if b_prime in S[B] and c not in S[A]:
                    S[A].add(c); changed = True

CR3 reads axiom (4) and adds the role edge $(\text{Professor}, \text{Student})$ to $R(\text{advises})$. Then CR4 reads axiom (5) — in normal form $\exists\text{advises}.\top \sqsubseteq \text{Researcher}$ — and, since $\top \in S(\text{Student})$ always holds, fires on that very edge to add Researcher to $S(\text{Professor})$. The subsumption Professor ⊑ Researcher is therefore doubly entailed, once by the hierarchy and once by the roles, and the completion algorithm finds both. This is why the run also reports a derived advises edge $(\text{Professor}, \text{Student})$ alongside its role-chain output grandAdvisor: [('Dean', 'Student'), …]: the little language is quietly composing existentials, chaining roles, and propagating consequences, not merely walking a tree. The restraint costs you expressiveness, but it does not cost you inference.

The payoff in the wild: SNOMED CT and the Gene Ontology

The academic world has ten concepts; the argument for EL is that the same algorithm, unchanged, classifies ontologies more than four orders of magnitude larger. SNOMED CT, the clinical terminology used in health systems worldwide, defines on the order of 350,000 concepts almost entirely with conjunction and existential restriction — exactly EL's three moves — because a clinical definition ("appendicitis is an inflammation located in some appendix") is naturally a positive conjunction of existential constraints, never a disjunction or a negation [1]. The Gene Ontology, describing tens of thousands of biological processes, molecular functions, and cellular components, has the same shape. Both are classified in practice by dedicated EL reasoners — ELK, CEL, and others — that implement precisely the completion loop above, and both classify in minutes on commodity hardware. That is the deployed argument for a small logic: an ExpTime tableau reasoner that is beautiful on a textbook TBox can choke on a real one, while the "impoverished" EL reasoner finishes, every time, because its worst case is a polynomial and not an exponential. The restraint is not academic modesty; it is the engineering decision that made web-scale biomedical ontologies reason-able at all.

The unsolved part

EL's polynomial guarantee is real but fragile at the edges, and the honest open question is exactly how far you can push the language before it snaps. EL++ is already near the maximal tractable extension: adding even seemingly innocent constructors breaks it. Universal restriction $\forall r.C$, disjunction $C \sqcup D$, or negation $\neg C$ each single-handedly lift subsumption out of PTIME, and some combinations of otherwise-harmless features (certain interactions of range restrictions with nominals, for instance) turn subsumption from tractable to intractable or even undecidable [3]. So the frontier is not a clean wall but a jagged coastline: EL++ sits just inside it, and mapping which additions stay polynomial, which jump to ExpTime, and which fall off into undecidability is genuinely intricate and not fully closed. The deeper unease for a neuro-symbolic reader is that the constructors EL bans — "not," "or," "only" — are exactly the ones natural knowledge often needs. A logic cheap enough to run on a million concepts may be too weak to say what a domain expert means, and no amount of reasoner engineering closes that gap; it is a property of the language, not the implementation.

Why it matters

The EL family is the first clean example in this book of a lesson the whole neuro-symbolic program keeps relearning: you buy scalability with a principled loss of expressiveness, and the art is choosing the loss on purpose. EL does not accidentally fail to express disjunction; it refuses to, because that refusal is what keeps its fixpoint polynomial and its reasoning exhaustive. That is the same trade a knowledge-graph embedding makes when it approximates instead of proving, only here the loss is exact and known in advance — you can say precisely what EL cannot conclude. When later volumes attach a neural learner to a symbolic reasoner, EL is the natural symbolic half to attach it to, because its guarantees are cheap, complete, and total: it classifies every concept, always halts, and never blows up. A hybrid system that must call its reasoner thousands of times inside a training loop cannot afford an ExpTime oracle; it can afford an EL one. The small logic is not a compromise you tolerate — it is the enabling condition for putting reasoning inside learning at all.

Key terms

• EL — the description logic with exactly three constructors: top $\top$, conjunction $\sqcap$, and existential restriction $\exists r.C$; no negation, disjunction, or universal restriction.
• EL++ — the tractable extension of EL, adding bottom $\bot$ (hence disjointness), role inclusions $r \sqsubseteq s$, role chains $r \circ s \sqsubseteq t$, nominals $\{a\}$, and the ABox — all present in the academic world.
• Subsumption — the core decision $C \sqsubseteq D$, "is every $C$ necessarily a $D$"; PTIME for the EL family, ExpTime and worse for expressive DLs.
• Bottom $\bot$ / unsatisfiable — the empty concept; deriving $A \sqsubseteq \bot$ means $A$ can have no instances, the reasoner's way of catching a self-contradictory definition (TenuredStudent, TenuredStudentAdvisor).
• Completion / saturation — the fixpoint algorithm that reads concept-inclusion axioms in four normal forms (keeping role inclusions and chains as-is) and fires the six rules CR1–CR4, CR⊥, CRχ until nothing new is derived; polynomial, and sound and complete for the EL fragment exercised here (bottom, role inclusions, role chains) — full EL++ with nominals and concrete domains needs a few more rules.
• Normal form — one of NF1–NF4, the restricted concept-inclusion shapes the completion rules match on; the 14 academic-world axioms normalize into 16 (six NF1, two NF2, three NF3, four NF4, plus the lone role chain kept unchanged).
• Role chain — a complex role inclusion $r \circ s \sqsubseteq t$; advises ∘ advises ⊑ grandAdvisor is the academic world's example, processed by CRχ rather than any normal form.
• Classification — computing all entailed subsumptions between named concepts; the academic world yields 8.

Where this leads

EL is one point in a whole space of tractable description logics, each trading expressiveness for a different guarantee. The standards body that governs OWL did not bless EL alone; it carved out three lightweight sublanguages — one tuned for very large class hierarchies like SNOMED CT, one for query answering over huge datasets, and one for rule-style reasoning — each a different answer to the same "keep it cheap" pressure. The next chapter, OWL 2 Profiles, maps those three fragments side by side: what each keeps, what each throws away, and which real task each was designed to make fast. EL is the profile you have now met in full; its two siblings are next.