Normalization: Reducing to Normal Forms

📍 Where we are: Part III · The EL Completion Algorithm — Chapter 8. The Complexity of Reasoning promised that EL subsumption is decidable in polynomial time; this chapter takes the first step of the algorithm that cashes that promise — reshaping the ontology so a fixed set of rules can fire mechanically.

The previous chapter told you that EL reasoning is cheap. This chapter starts showing how. Before the completion rules of the next chapter can grind the terminology to a fixpoint, the reasoner does something almost boring on purpose: it rewrites every axiom into one of a tiny handful of rigid shapes. Nothing is proved yet; the ontology is only reshaped, like flattening a stack of oddly-folded letters into standard fill-in-the-blank forms so a clerk can stamp them without reading. That flattening is normalization, and it is what makes the rest of the machinery run in constant time per step.

The simple version

Imagine a customs officer who is only allowed to stamp four kinds of form. You arrive with a rambling handwritten request full of nested clauses ("anyone who advises an author-of-a-paper counts as a person"). The officer will not read it as prose. Instead they hand you four blank templates, each with one blank to fill, and make you re-copy your request onto them — and whenever a phrase is too big to fit one line, you invent a short reference code for it and file the code's meaning on its own separate form. Once every request sits on a standard template, stamping becomes instant and thoughtless. Normalization is exactly this re-copying step, done to logic axioms instead of paperwork.

What this chapter covers

• Why normalize at all — the completion rules must recognize an axiom's shape in constant time; arbitrarily nested concepts would make them unwieldy, so normalization is the simplifying preprocessing that pays for the polynomial guarantee.
• The four normal forms — NF1 through NF4, decoded in plain words and then in real description-logic notation, plus the role chains that are kept untouched.
• Basic concepts — the "leaf" pieces a normal form is allowed to contain: a concept name, ⊤ (top), or ⊥ (bottom).
• Fresh names and conservative extension — why inventing a new symbol Ĉ for a compound subconcept adds no new consequences about the original vocabulary.
• The rewrite rules as a worklist — the six-clause loop in the companion code that pops each axiom, splits or names the offending piece, and pushes the leftovers back until everything is normal.
• The academic world, normalized — two deliberately non-normal axioms forcing exactly two fresh names, and the real run: 14 axioms grow to 16.

Why normalize before you reason

The engine of Volume 2 is a completion algorithm — a monotone operator iterated to a fixpoint, the same shape as the forward-chaining operator of Volume 1, now over subsumption facts (el_completion.py lines 32–33). Each pass scans the axioms and, for every one whose pattern is met, records a new consequence. For that scan to be cheap, the rule must decide "does this axiom apply here?" in O(1) — constant time, independent of how big the ontology is. An axiom like

$$\exists \text{advises}.(\exists \text{authored}.\text{Paper}) \sqsubseteq \text{Person}$$

cannot be matched in constant time: it nests an existential inside an existential, and a rule would have to recurse into that structure every time it fired. The fix is to guarantee, before reasoning starts, that every axiom already has one of a few flat shapes with no nesting to walk into. Then each completion rule is a single pattern-match against a fixed template. Normalization is that guarantee, bought once up front [1].

Normalization flattens nested axioms into four rigid templates, inventing fresh names _N1 and _N2 for the compound subconcepts, and the academic world's fourteen axioms become sixteen. Original diagram by the authors, created with AI assistance.

The four normal forms

A concept in EL can be a name (a capitalized atom such as Professor), the top concept ⊤ (which every individual belongs to), the bottom concept ⊥ (which nothing belongs to), or a compound built with the two EL constructors — conjunction $C \sqcap D$ ("both a $C$ and a $D$") and existential restriction $\exists r.C$ ("related by role $r$ to some $C$"). The trouble is compounds nest arbitrarily deep. A normal form forbids that nesting: it is one of exactly four axiom templates whose slots hold only basic concepts.

A basic concept is the simplest kind — a name, ⊤, or ⊥, with no constructor on top. The companion defines it in one line (ontology.py lines 92–95):

def is_basic(c) -> bool:
    """A *basic* concept is a name or ⊤/⊥ — the only thing allowed on the "leaf"
    positions of the four EL normal forms."""
    return is_name(c)

With "basic" in hand, here are the four forms. Read $A \sqsubseteq B$ as "every $A$ is a $B$" (the symbol ⊑ is subsumption, subclass-of); $A_1 \sqcap A_2$ as "both an $A_1$ and an $A_2$"; and $\exists r.B$ as "advises/authored/… some $B$". The letters $A, A_1, A_2, B$ each stand for a basic concept, and $r$ for a role:

$$\text{NF1: } A \sqsubseteq B \qquad \text{NF2: } A_1 \sqcap A_2 \sqsubseteq B \qquad \text{NF3: } A \sqsubseteq \exists r.B \qquad \text{NF4: } \exists r.B \sqsubseteq A$$

tag	normal form	in words
NF1	$A \sqsubseteq B$	one basic concept sits under another
NF2	$A_1 \sqcap A_2 \sqsubseteq B$	a conjunction of basics sits under a basic
NF3	$A \sqsubseteq \exists r.B$	a basic sits under an existential with a basic filler
NF4	$\exists r.B \sqsubseteq A$	an existential with a basic filler sits under a basic

Two things live outside the four forms and are simply kept as-is: role chains $r \circ s \sqsubseteq t$ ("doing $r$ then $s$ counts as doing $t$", the ∘ read "composed with") and simple role inclusions $r \sqsubseteq s$. They are already flat — their slots are role names, not concepts — so there is nothing to normalize. The completion rules of the next chapter have roughly one matcher per row of that table, plus matchers for chains and the bottom concept, and every matcher is O(1) precisely because every slot is guaranteed basic.

Fresh names: a conservative extension

The forms above are strict, so most real axioms violate them. What do you do with a compound subconcept like $\exists \text{authored}.\text{Paper}$ that has no business sitting inside a slot? You name it away. Invent a brand-new concept name — call it $\hat{C}$ — declare that it means the compound, and substitute the name into the slot. The companion mints these names with a tiny counter (el_completion.py lines 54–66):

class _Fresh:
    """A factory of fresh, internal concept names ``_N1, _N2, ...`` introduced to
    stand for the compound subconcepts that normalization must name away."""

    def __init__(self):
        self.n = 0
        self.names = []

    def __call__(self) -> str:
        self.n += 1
        name = f"_N{self.n}"
        self.names.append(name)
        return name

The worry is obvious: does bolting new symbols onto the ontology change what it says? It does not, and the reason has a name. Normalization is a conservative extension [2]: the rewritten TBox $T'$ entails exactly the same subsumptions between original names as the starting TBox $T$ did. Writing $\Sigma$ for the original vocabulary (the concepts and roles you started with, before any $\hat{C}$), the guarantee is

$$T \models (A \sqsubseteq B) \quad\Longleftrightarrow\quad T' \models (A \sqsubseteq B) \qquad \text{for all } A, B \in \Sigma.$$

Adding the definition $\hat{C} \equiv \exists \text{authored}.\text{Paper}$ can only produce new facts that mention $\hat{C}$; it can never invent a new relationship between two old names, because $\hat{C}$ is fresh — nothing else refers to it. (In practice the code is even thriftier: depending on whether the compound appeared on the left or the right of ⊑, it adds only the one direction of that equivalence the polarity needs — here $\exists \text{authored}.\text{Paper} \sqsubseteq \hat{C}$ — which is all that is required to preserve entailments.) So classification can read its answers off the completed model and simply hide any name starting with _N, confident the hidden names changed nothing about the visible ones.

The rewrite rules as a worklist

normalize (el_completion.py lines 69–154) is a worklist to a fixpoint: a to-do list of general concept inclusions (GCIs — the axioms $L \sqsubseteq R$) that starts as the whole TBox and shrinks until every entry is normal. Role chains and role inclusions are already flat, so they go straight to the output; every GCI goes on the worklist:

    fresh = _Fresh()
    out = []
    work = []           # worklist of GCIs (L, R) still to normalize

    for ax in tbox:
        if ax[0] == "⊑":
            work.append((ax[1], ax[2]))
        elif ax[0] == "∘⊑":
            out.append(("chain", ax[1], ax[2]))
        elif ax[0] == "r⊑":
            out.append(("rsub", ax[1], ax[2]))

The loop then pops one GCI at a time and applies the first rewrite that fits. Each rewrite either splits the axiom or names one offending piece, pushing smaller GCIs back onto the worklist — so the list can grow before it shrinks, exactly like the fixpoint climbs of the previous part. There are six clauses; the two that the academic world triggers are naming a compound filler of a left-hand existential, and naming a compound conjunct of a left-hand conjunction:

        # (d) Name a compound filler of a LEFT existential (negative position):
        #     ∃r.Ĉ ⊑ R  ⟶  ∃r.A ⊑ R,  Ĉ ⊑ A   (A fresh).
        if is_some(L) and not is_basic(L[2]):
            a = fresh()
            work.append((("∃", L[1], a), R))
            work.append((L[2], a))
            continue

        # (e) Name each compound conjunct of a LEFT conjunction:
        #     ... ⊓ Ĉ ⊓ ... ⊑ R  ⟶  replace Ĉ by fresh A, add Ĉ ⊑ A.
        if is_and(L) and any(not is_basic(c) for c in L[1]):
            new_conjuncts = []
            for c in L[1]:
                if is_basic(c):
                    new_conjuncts.append(c)
                else:
                    a = fresh()
                    work.append((c, a))
                    new_conjuncts.append(a)
            work.append((("⊓", tuple(new_conjuncts)), R))
            continue

The other clauses handle the remaining shapes: splitting a right-hand conjunction $L \sqsubseteq C \sqcap D$ into $L \sqsubseteq C$ and $L \sqsubseteq D$, naming compound fillers of a right-hand existential, and — when the right side is an existential but the left is still compound — naming the whole existential so the left can be normalized on its own. When a popped GCI has no compound left to attack, the final clause reads off which of the four templates it matches and emits the tagged tuple (el_completion.py lines 142–152):

        # (f) Now L and R are simple enough — emit the matching normal form.
        if is_basic(L) and is_basic(R):
            out.append(("nf1", L, R))
        elif is_and(L) and is_basic(R):
            out.append(("nf2", tuple(L[1]), R))
        elif is_basic(L) and is_some(R):
            out.append(("nf3", L, R[1], R[2]))
        elif is_some(L) and is_basic(R):
            out.append(("nf4", L[1], L[2], R))
        else:  # pragma: no cover - defensive; the rules above are exhaustive
            raise ValueError(f"cannot normalize {render(L)} ⊑ {render(R)}")

Each rewrite strictly shrinks the total nesting depth of the pending GCIs, so the worklist cannot loop forever: it empties in time linear in the size of the TBox [3].

The academic world, normalized

Twelve of the fourteen axioms in the running ontology are born normal. Professor ⊑ Researcher is already NF1; Professor ⊑ ∃advises.Student is already NF3 (its filler Student is basic); Professor ⊓ Student ⊑ ⊥ is already NF2; the role chain advises ∘ advises ⊑ grandAdvisor is kept untouched. Two axioms were planted deliberately off-form so normalization visibly has work to do (ontology.py lines 165–173):

$$(13)\quad \exists \text{advises}.(\exists \text{authored}.\text{Paper}) \sqsubseteq \text{Person}$$ $$(14)\quad \text{Person} \sqcap \exists \text{authored}.\text{Paper} \sqsubseteq \text{Researcher}$$

Axiom (13) is a left-hand existential whose filler $\exists \text{authored}.\text{Paper}$ is compound, so clause (d) fires: it mints _N2 for the filler, leaving $\exists \text{advises}.\_N2 \sqsubseteq \text{Person}$ (NF4) and $\exists \text{authored}.\text{Paper} \sqsubseteq \_N2$ (again NF4). Axiom (14) is a left-hand conjunction with a compound conjunct, so clause (e) fires: it mints _N1 for that conjunct, leaving $\text{Person} \sqcap \_N1 \sqsubseteq \text{Researcher}$ (NF2) and $\exists \text{authored}.\text{Paper} \sqsubseteq \_N1$ (NF4). The four tagged tuples the code actually emits for these two axioms are:

('nf2', ('Person', '_N1'), 'Researcher')      # Person ⊓ _N1 ⊑ Researcher   (from axiom 14)
('nf4', 'authored', 'Paper', '_N1')            # ∃authored.Paper ⊑ _N1        (from axiom 14)
('nf4', 'authored', 'Paper', '_N2')            # ∃authored.Paper ⊑ _N2        (from axiom 13)
('nf4', 'advises', '_N2', 'Person')            # ∃advises._N2 ⊑ Person        (from axiom 13)

Notice that _N1 and _N2 abbreviate the same compound, $\exists \text{authored}.\text{Paper}$ — the normalizer mints a separate fresh name for each occurrence rather than sharing one. That is why two non-normal axioms cost two fresh names, not one. Running the module prints the tally and the census by form (el_completion.py lines 328–334):

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}

Twelve already-normal axioms plus the four produced from (13) and (14) give sixteen, and they distribute across the forms exactly as the census reports:

normal form	axiom shape	count
chain	$r \circ s \sqsubseteq t$	1
NF1	$A \sqsubseteq B$	6
NF2	$A_1 \sqcap A_2 \sqsubseteq B$	2
NF3	$A \sqsubseteq \exists r.B$	3
NF4	$\exists r.B \sqsubseteq A$	4
total		16

The TBox is now nothing but sixteen flat templates and one role chain — a shape the completion rules can chew through in constant time per firing.

The unsolved part

The honest limit of this chapter is that normalization does no reasoning whatsoever. It has not decided a single subsumption; it has not noticed that TenuredStudent is unsatisfiable or that Dean ⊑ Researcher. It has only reshaped the ontology, trading two nested axioms for four flat ones and two invented names. Every genuine inference — every new ⊑ fact — is still to come, and it comes only when the completion rules saturate these normalized axioms to a fixpoint. The little redundancy we spotted (two names for one compound) is a symptom of the same modesty: normalization is a syntactic pass with no semantic memory, so it will not fold equal subconcepts together, and a smarter reasoner leaves that to the reasoning step that follows. Normalization is the flat, dependable runway; the flight is the next chapter.

Why it matters

The move here — reduce arbitrary structure to a small fixed set of templates so a mechanical operator can act on it uniformly — is one of the deepest recurring habits in neuro-symbolic AI, not a quirk of EL. A neural reasoner that consumes logical structure needs its inputs in a canonical shape for the same reason a completion rule does: a fixed-arity, no-nesting encoding is what lets a single learned or hand-written operator apply everywhere without special-casing depth. When later volumes feed ontologies to embeddings or to differentiable provers, they will normalize first, for exactly the motive here — a rigid template is the shared substrate on which a symbolic rule and a neural layer can both operate. Getting the crisp version right, and knowing it changed no meaning (the conservative-extension guarantee), is precisely the yardstick against which any softer, learned reshaping must be judged.

Key terms

• Normalization — rewriting a TBox so every axiom is one of four normal forms plus role chains, introducing fresh names for compound subconcepts.
• Normal form (NF1–NF4) — the four allowed axiom templates: $A \sqsubseteq B$, $A_1 \sqcap A_2 \sqsubseteq B$, $A \sqsubseteq \exists r.B$, $\exists r.B \sqsubseteq A$, with every slot a basic concept.
• Basic concept — the leaf pieces a normal form may contain: a concept name, ⊤ (top), or ⊥ (bottom); no constructor on top.
• Fresh name ($\hat{C}$) — a brand-new symbol (_N1, _N2, …) that abbreviates a compound subconcept so it can occupy a slot.
• Conservative extension — the guarantee that the rewritten TBox entails exactly the same subsumptions between original names as the original, so fresh names add no new consequences over the old vocabulary.
• Worklist — the shrinking to-do list of not-yet-normal GCIs that normalize pops, splits or names, and pushes back until it empties.
• Role chain — a complex role inclusion $r \circ s \sqsubseteq t$, kept as-is because it is already flat.

Where this leads

The ontology is now sixteen flat axioms, each in a shape a rule can match without ever looking inside it — but not one subsumption has been decided yet. The next chapter, Completion Rules, turns these templates into inference: it defines the two data structures $S(A)$ and $R(r)$, fires the rules CR1–CR4, the bottom rule, and the role-chain rule until nothing new appears, and reads the full classification of the academic world — including the unsatisfiability of TenuredStudent — straight off the saturated result. Normalization built the runway; completion is the reasoning that finally takes off.