Completion Rules: CR1–CR4 and the Bottom Rule

📍 Where we are: Part III · The EL Completion Algorithm — Chapter 9. Normalization flattened all 14 TBox axioms into 16 axioms of just four shapes plus role chains; now we feed those flat shapes to an engine that fires them over and over until the ontology has told us everything it entails.

Normalization did the boring, essential work: it guaranteed that every axiom the reasoner will ever look at matches one of a tiny, fixed set of patterns, so the reasoner never has to parse a deeply nested concept. This chapter builds the reasoner that consumes those patterns. It is astonishingly small — one while loop firing six named completion rules (CR1–CR4, CR⊥, CRχ) plus a trivial role-inclusion copy rule — and yet it is a complete classifier for the EL family of description logics, the logic behind biomedical ontologies with hundreds of thousands of classes. The whole trick is to stop reasoning about concepts and start growing two tables until they stop growing.

The simple version

Imagine a gossip network in a department. Each person keeps two lists on a card: "clubs I'm secretly a member of" and "people I'm known to have a certain kind of tie to." You hand everyone the department bylaws — "any member of the Chess Club is also a member of the Games Society," "anyone who mentors a professor mentors a researcher" — and let them gossip. Whenever a rule lets someone add a club or a tie they didn't have written down, they scribble it in. Nobody erases anything. You keep the room buzzing until one full round of gossip adds not a single new line to anyone's card. At that instant the room is saturated: every membership and every tie that follows from the bylaws is now written down, and you can read any conclusion straight off a card. That saturated state is the answer, and the completion rules are the bylaws.

What this chapter covers

The two tables you saturate — $S(A)$ , the basic concepts $A$ is known to be a kind of, and $R(r)$ , the concept-pairs joined by an $\exists r$ edge; both start almost empty and only grow.
The six rules in one block — CR1–CR4 keyed one-to-one to normal forms NF1–NF4, plus the bottom rule CR⊥ and the role-chain rule CRχ.
The engine itself — the real while changed loop from the companion file, and why "changed" is exactly the fixpoint test $T(X) = X$ of Volume 1's forward chaining.
A derivation by hand — how axioms (4) and (5) re-derive Professor ⊑ Researcher through the roles via CR3 then CR4, and how the role chain manufactures a grandAdvisor edge.
The bottom rule earning its keep — how disjointness makes ⊥ ∈ S(TenuredStudent), and how ⊥ then crawls backward along advises to condemn TenuredStudentAdvisor.
The fixpoint, measured — the academic world settles at $|S| = 39$ , $|R| = 7$ in three rounds, quoted from the real run and summarized in a rule-by-rule table.
The unsolved part — the rules plainly derive true things, but do they derive all true subsumptions, and only true ones? That is soundness and completeness, the next chapter.

The two tables: S(A) and R(r)

The completion algorithm maintains exactly two data structures, and understanding them is most of the battle. Read the notation this way before the symbols arrive: think of $S$ and $R$ as two ledgers the reasoner writes into, never erasing.

The first ledger, $S(A)$ , holds — for each basic concept $A$ (a concept name, or the special ⊤ "everything" or ⊥ "nothing") — the set of basic concepts that $A$ is currently known to be subsumed by. Read $B \in S(A)$ as the standing claim " $A \sqsubseteq B$ ," i.e. "everything that is an $A$ is also a $B$ ." So $S(\text{Professor})$ is literally the list of all the things a professor is provably a kind of.

The second ledger, $R(r)$ , holds — for each role $r$ — the set of concept-pairs $(A, B)$ such that every $A$ is known to be joined by an $r$ -edge to some $B$ . Read $(A, B) \in R(r)$ as " $A \sqsubseteq \exists r.B$ ," i.e. "every $A$ stands in relation $r$ to at least one $B$ ." So $(\text{Professor}, \text{Student}) \in R(\text{advises})$ records the derived fact that every professor advises some student.

Both ledgers start at their smallest honest value. Every concept is a kind of itself and a kind of ⊤, so we seed

S(A) \;=\; \{\, A,\ \top \,\} \qquad\text{for every basic concept } A,

and we start $R(r) = \varnothing$ for every role — no edges are known before any rule fires. In the companion file this is two lines (el_completion.py lines 185–189): S = {a: {a, TOP} for a in names} and R = {}. In the academic world there are 12 basic-concept keys — the 8 named concepts that survive into the normalized axioms, the 2 fresh names $\_N1, \_N2$ that normalization invented, plus ⊤ and ⊥ — so the seed already holds 23 subsumption entries (⊤'s own set is just $\{\top\}$ , one short of the pairwise count) and 0 role pairs. That $(23, 0)$ is the starting line of the saturation trace we will read off at the end.

The six rules, keyed to the four normal forms

Each completion rule is an if-present-then-add implication: if certain entries are already in the ledgers and a matching axiom exists, add one more entry. Four of the six rules correspond one-to-one to the four normal forms NF1–NF4 that normalization produced; the last two handle disjointness (⊥) and role chains. Here is the full set [1], with $A', B', C$ ranging over basic concepts and $r, s, t$ over roles:

\begin{aligned} \textbf{CR1:}\;\; A' \in S(A),\; A' \sqsubseteq B \;&\Longrightarrow\; B \in S(A) \\ \textbf{CR2:}\;\; A_1, A_2 \in S(A),\; A_1 \sqcap A_2 \sqsubseteq B \;&\Longrightarrow\; B \in S(A) \\ \textbf{CR3:}\;\; A' \in S(A),\; A' \sqsubseteq \exists r.B \;&\Longrightarrow\; (A, B) \in R(r) \\ \textbf{CR4:}\;\; (A, B) \in R(r),\; B' \in S(B),\; \exists r.B' \sqsubseteq C \;&\Longrightarrow\; C \in S(A) \\ \textbf{CR}\bot\textbf{:}\;\; (A, B) \in R(r),\; \bot \in S(B) \;&\Longrightarrow\; \bot \in S(A) \\ \textbf{CR}\chi\textbf{:}\;\; (A, B) \in R(r),\; (B, C) \in R(s),\; r \circ s \sqsubseteq t \;&\Longrightarrow\; (A, C) \in R(t) \end{aligned}

Decode them one at a time. CR1 is transitivity of subsumption along an NF1 axiom $A' \sqsubseteq B$ : if $A$ is already known to be an $A'$ , and every $A'$ is a $B$ , then $A$ is a $B$ . CR2 handles a conjunction (NF2 axiom $A_1 \sqcap A_2 \sqsubseteq B$ ): if $A$ is known to be both an $A_1$ and an $A_2$ , it inherits $B$ . CR3 introduces a role edge from an NF3 axiom $A' \sqsubseteq \exists r.B$ : knowing $A$ is an $A'$ lets us record that $A$ has an $r$ -edge to a $B$ . CR4 is the subtle one — the elimination of an existential using an NF4 axiom $\exists r.B' \sqsubseteq C$ : if $A$ has an $r$ -edge into some $B$ , and that $B$ is known to be a $B'$ , and anything with an $r$ -edge into a $B'$ must be a $C$ , then $A$ is a $C$ . It reads the edge ledger and writes back into the subsumer ledger, which is how information flows from $R$ back into $S$ . CR⊥, the bottom rule, propagates unsatisfiability across an edge: if $A$ has an $r$ -edge to a $B$ that has turned out to be impossible ( $\bot \in S(B)$ ), then $A$ is impossible too — you cannot have an edge to something that cannot exist. CRχ, the role-chain rule, composes two edges through an axiom $r \circ s \sqsubseteq t$ : an $r$ -edge from $A$ to $B$ followed by an $s$ -edge from $B$ to $C$ yields a $t$ -edge from $A$ to $C$ .

The completion engine: six rules read the normalized axioms and grow the two ledgers S(A) and R(r), looping until a full pass adds nothing — the fixpoint where the academic world holds 39 subsumer entries and 7 role edges. Original diagram by the authors, created with AI assistance.

The engine: fire every rule until nothing changes

The rules above are declarative — they say what may be added, not when. The engine supplies the "when" with the simplest possible control structure: a loop that keeps firing every rule until a full pass adds nothing. First it buckets the normalized axioms by shape so each rule scans only the axioms it can match (el_completion.py lines 190–196):

    # Bucket the axioms by shape so each rule scans only what it needs.
    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"]

Then the fixpoint loop. A single boolean, changed, records whether any rule added any entry during the current pass; the loop repeats exactly while that stays true (el_completion.py lines 211–244):

    changed = True
    while changed:
        changed = False

        # CR1: A' ∈ S(A), A' ⊑ B  ⟹  B ∈ S(A)
        for _, a_prime, b in nf1:
            for A in names:
                if a_prime in S[A] and b not in S[A]:
                    S[A].add(b); changed = True

        # CR2: A1, A2 ∈ S(A), A1 ⊓ A2 ⊑ B  ⟹  B ∈ S(A)
        for _, conj, b in nf2:
            for A in names:
                if b not in S[A] and all(c in S[A] for c in conj):
                    S[A].add(b); changed = True

        # 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

        # CR⊥ (the bottom rule): (A, B) ∈ R(r), ⊥ ∈ S(B)  ⟹  ⊥ ∈ S(A)
        for r, pairs in list(R.items()):
            for (A, B) in list(pairs):
                if BOT in S[B] and BOT not in S[A]:
                    S[A].add(BOT); changed = True

The pattern is exactly the immediate-consequence operator $T_P$ of Volume 1, now iterating over subsumption facts instead of ground atoms [2]. Bundle the whole body of the loop into one operator $T$ that takes the current pair of ledgers $(S, R)$ and returns them enlarged by one round of every rule. Because no rule ever removes an entry — every rule only calls S[A].add(...) or add_r(...), never a delete — $T$ is monotone: a bigger input state can only produce a bigger output state. That is the single property Knaster–Tarski and the Kleene climb of Volume 1 needed, so the loop is the same construction: seed at the bottom, apply the monotone $T$ repeatedly, and stop at the least fixpoint, the smallest state closed under all the rules. The exit test while changed is precisely the fixpoint condition $T(X) = X$ made executable: changed stays False for a whole pass exactly when applying every rule adds nothing, i.e. when the state maps to itself. The docstring says as much in one line — "The whole thing is just a fixpoint of a monotone operator — the very same shape as the forward-chaining T_P of Volume 1" (el_completion.py lines 32–33).

Two more rule blocks finish each pass. The simple role-inclusion rule copies an edge along an axiom $r \sqsubseteq s$ ; the role-chain rule CRχ composes two edges through $r \circ s \sqsubseteq t$ (el_completion.py lines 246–257):

        # Simple role inclusions r ⊑ s:  (A,B) ∈ R(r)  ⟹  (A,B) ∈ R(s)
        for _, r, s in rsubs:
            for pair in list(R.get(r, ())):
                if add_r(s, pair):
                    changed = True

        # CRχ (role chain): (A,B) ∈ R(r), (B,C) ∈ R(s), r ∘ s ⊑ t  ⟹  (A,C) ∈ R(t)
        for _, (r, s), t in chains:
            for (A, B) in list(R.get(r, ())):
                for (B2, C) in list(R.get(s, ())):
                    if B == B2 and add_r(t, (A, C)):
                        changed = True

The role-inclusion block does nothing on the academic world — rsubs is empty because the TBox has no $r \sqsubseteq s$ axioms — but it belongs to the loop, so the engine really fires seven rule blocks per pass, of which six are the named rules CR1–CR4, CR⊥, and CRχ.

A derivation by hand: the roles re-derive Professor ⊑ Researcher

Watch the two existential rules cooperate on the academic world's most instructive pair of axioms. After normalization, axiom (4) "every professor advises some student" is the NF3 axiom ("nf3", "Professor", "advises", "Student"), i.e. $\text{Professor} \sqsubseteq \exists\text{advises}.\text{Student}$ , and axiom (5) "anyone who advises anything is a researcher" is the NF4 axiom ("nf4", "advises", "⊤", "Researcher"), i.e. $\exists\text{advises}.\top \sqsubseteq \text{Researcher}$ . Neither says "Professor ⊑ Researcher" outright; together they force it, and the completion rules find it:

CR3 fires on axiom (4). The seed already put $\text{Professor} \in S(\text{Professor})$ , so with $A' = A = \text{Professor}$ and the axiom $\text{Professor} \sqsubseteq \exists\text{advises}.\text{Student}$ , CR3 adds the edge $(\text{Professor}, \text{Student})$ to $R(\text{advises})$ . The reasoner now knows every professor advises some student.
CR4 fires on axiom (5). We now have $(\text{Professor}, \text{Student}) \in R(\text{advises})$ ; the required $B' = \top$ sits in $S(\text{Student})$ automatically (⊤ is in every seed); and the axiom is $\exists\text{advises}.\top \sqsubseteq \text{Researcher}$ . So CR4 adds $\text{Researcher}$ to $S(\text{Professor})$ . The existential got eliminated: an edge plus an NF4 axiom produced a new subsumer.
CR1 cascades. With $\text{Researcher} \in S(\text{Professor})$ and the NF1 axiom $\text{Researcher} \sqsubseteq \text{Person}$ , CR1 adds $\text{Person}$ to $S(\text{Professor})$ .

The reasoner has re-derived $\text{Professor} \sqsubseteq \text{Researcher} \sqsubseteq \text{Person}$ through a completely different route than the direct hierarchy axiom (1) — through the roles — and the two routes agree. The saturated ledger confirms it exactly: S[Professor] = ['Person', 'Professor', 'Researcher', '⊤'].

The role chain rides on the same edges. A dean is a professor (axiom 8, NF1) who advises some professor (axiom 9, NF3), so CR3 puts $(\text{Dean}, \text{Professor})$ into $R(\text{advises})$ ; and because Dean inherits Professor via CR1, CR3 on axiom (4) also puts $(\text{Dean}, \text{Student})$ there. Now CRχ, matching the chain axiom $\text{advises} \circ \text{advises} \sqsubseteq \text{grandAdvisor}$ , finds the edge $(\text{Dean}, \text{Professor})$ in $R(\text{advises})$ followed by $(\text{Professor}, \text{Student})$ in $R(\text{advises})$ , sharing the middle concept Professor, and fuses them into $(\text{Dean}, \text{Student}) \in R(\text{grandAdvisor})$ — a dean is the grand-advisor of a student, derived purely from the schema.

The bottom rule earning its keep

The five rules so far only ever add true memberships. The bottom rule is what lets the reasoner detect contradictions — concepts that can have no instances at all. The academic world was rigged to trigger it twice.

First, directly, on TenuredStudent. Axioms (10) and (11) make it both a professor and a student — normalized to two NF1 axioms $\text{TenuredStudent} \sqsubseteq \text{Professor}$ and $\text{TenuredStudent} \sqsubseteq \text{Student}$ — while axiom (6), disjointness, is the NF2 axiom $\text{Professor} \sqcap \text{Student} \sqsubseteq \bot$ :

CR1 twice adds both $\text{Professor}$ and $\text{Student}$ to $S(\text{TenuredStudent})$ .
CR2 fires on the disjointness axiom: with $A_1 = \text{Professor}$ and $A_2 = \text{Student}$ both in $S(\text{TenuredStudent})$ and the axiom $\text{Professor} \sqcap \text{Student} \sqsubseteq \bot$ , it adds $\bot$ to $S(\text{TenuredStudent})$ .

Having $\bot \in S(\text{TenuredStudent})$ means "TenuredStudent ⊑ ⊥" — the concept is unsatisfiable, provably empty in every model. This is the classic "you modelled one class two incompatible ways" bug that an EL reasoner catches for you.

Second, and more delicately, ⊥ propagates backward along a role to TenuredStudentAdvisor. Axiom (12) is the NF3 axiom $\text{TenuredStudentAdvisor} \sqsubseteq \exists\text{advises}.\text{TenuredStudent}$ :

CR3 fires, adding the edge $(\text{TenuredStudentAdvisor}, \text{TenuredStudent})$ to $R(\text{advises})$ .
CR⊥ fires. With that edge in $R(\text{advises})$ and $\bot \in S(\text{TenuredStudent})$ from step 2, the bottom rule adds $\bot$ to $S(\text{TenuredStudentAdvisor})$ .

The reasoning is airtight: a tenured-student-advisor must, by definition, advise some tenured student, but no tenured student can exist, so no tenured-student-advisor can exist either. The saturated ledger records exactly this: S[TenuredStudentAdvisor] contains ⊥, and the final classification reports both concepts as unsatisfiable. Note the order dependence that makes a fixpoint — not a single pass — necessary: the edge in step 3 and the emptiness in step 2 must both be present before CR⊥ can fire, so the engine must keep looping until every such interaction has had its chance.

The fixpoint, measured

Run the module on the academic world and it prints the saturation growing round by round to its fixpoint — this is 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 that each rise then plateau — the same wave shape as Volume 1's [23, 41, 47, 47] fact counts, except the two ledgers here do not climb in step: the edge ledger $R$ reaches its fixpoint a full round before the subsumer ledger $S$ . The subsumer ledger climbs $23 \to 34 \to 39 \to 39$ ; the edge ledger climbs $0 \to 7 \to 7 \to 7$ . Round 1 does almost all the work, because the fixed rule order CR1→CR2→CR3→CR4→CR⊥→CRχ lets a fact added early in a pass feed a later rule within the same pass. In one round it produces all 7 role edges (the five advises edges from CR3, and — once those exist — the two grandAdvisor edges from CRχ) and all 11 of round 1's new subsumers, and those 11 already include the hard cases: $\text{Professor} \sqsubseteq \text{Researcher}$ (added directly by CR1 from the hierarchy axiom, and re-derivable by CR4 through the roles), and both unsatisfiability marks — $\bot \in S(\text{TenuredStudent})$ from CR2 on the disjointness axiom, and $\bot \in S(\text{TenuredStudentAdvisor})$ from CR⊥ crawling backward along advises. Round 2 fires only the CR1 cascade that round 1 left with room to run: Dean, Professor, Student, TenuredStudent, and TenuredStudentAdvisor each already carry Researcher, so the NF1 axiom $\text{Researcher} \sqsubseteq \text{Person}$ adds Person to all five — the last 5 subsumers, and nothing else. Round 3 fires every rule once more, adds nothing, and so proves the fixpoint reached: $39 = 39$ and $7 = 7$ is the engine certifying to itself that it is done. The academic world saturates at $|S| = 39$ , $|R| = 7$ .

Reading the answer off those ledgers (the subject of Classification) yields 8 subsumptions between named concepts and 2 unsatisfiable concepts:

unsatisfiable concepts (2): ['TenuredStudent', 'TenuredStudentAdvisor']
derived role edges R:
  advises: [('Dean', 'Professor'), ('Dean', 'Student'), ('Professor', 'Student'), ('TenuredStudent', 'Student'), ('TenuredStudentAdvisor', 'TenuredStudent')]
  grandAdvisor: [('Dean', 'Student'), ('TenuredStudentAdvisor', 'Student')]

Here is the whole rulebook as a table, each row keyed to the normal form it consumes, the entries it needs present, and the entry it adds:

rule	consumes	precondition (already in ledgers)	adds
CR1	NF1 $A' \sqsubseteq B$	$A' \in S(A)$	$B \in S(A)$
CR2	NF2 $A_1 \sqcap A_2 \sqsubseteq B$	$A_1, A_2 \in S(A)$	$B \in S(A)$
CR3	NF3 $A' \sqsubseteq \exists r.B$	$A' \in S(A)$	$(A, B) \in R(r)$
CR4	NF4 $\exists r.B' \sqsubseteq C$	$(A, B) \in R(r)$ and $B' \in S(B)$	$C \in S(A)$
CR⊥	disjointness (⊥)	$(A, B) \in R(r)$ and $\bot \in S(B)$	$\bot \in S(A)$
CRχ	chain $r \circ s \sqsubseteq t$	$(A, B) \in R(r)$ and $(B, C) \in R(s)$	$(A, C) \in R(t)$

The reason this engine matters beyond a toy is its cost. With $n$ basic concept names, $S$ has at most $n$ keys each holding at most $n$ subsumers, so $|S| = O(n^2)$ ; each $R(r)$ holds at most $n^2$ pairs. Every rule firing adds at least one entry to a ledger that can never shrink and is bounded by $O(n^2)$ , so the loop runs only polynomially many productive rounds — the whole classification is polynomial, in fact cubic $O(n^3)$ time [3]. That polynomial bound, engineered into EL by keeping only ⊓ and ∃, is exactly why EL reasoners classify SNOMED CT and the Gene Ontology, ontologies with hundreds of thousands of classes, in seconds.

The unsolved part

Everything above shows the rules deriving things that are evidently true: each rule is a locally obvious implication, and we watched them cooperate to reach the right answer on a world we can check by eye. But "evidently true on this example" is not a proof of anything, and two genuine questions remain open at exactly this point. First, soundness: does every entry the rules ever add correspond to a subsumption that truly holds in every model of the TBox — or could some unlucky interaction of rules manufacture a $B \in S(A)$ that is not actually entailed? Second, and harder, completeness: when the loop halts because nothing changed, has it really found all the entailed subsumptions — or might there be some $A \sqsubseteq B$ that genuinely follows from the axioms yet no sequence of these rules can ever write into $S(A)$ ? A reasoner that is sound but incomplete would silently miss real conclusions; one that is complete but unsound would assert false ones. Neither failure is visible from a single passing example. The claim that these rules are exactly right — they derive all and only the true subsumptions — is a theorem that has to be earned, and earning it is the entire job of the next chapter.

Why it matters

The completion algorithm is the concrete payoff of the whole "reasoning as a fixpoint" story that Volume 1 set up abstractly. It shows that an industrial-strength description-logic reasoner is not a mysterious theorem-proving oracle but the same monotone-operator climb you already understand from forward chaining — just iterating over subsumption facts and role edges instead of ground atoms. For neuro-symbolic AI this is the crisp, checkable target a learned reasoner must hit: when a differentiable or embedding-based model claims to "reason over an ontology," the 39 subsumer entries and 7 edges this engine derives are the ground truth it should reproduce, and the unsatisfiability of TenuredStudentAdvisor is precisely the kind of long-range, contradiction-through-a-role inference that soft models tend to miss. Knowing exactly what the exact algorithm computes — and, next chapter, why it is exactly right — is what lets you say whether a neural approximation reached the correct fixpoint or merely a plausible-looking one.

Key terms

$S(A)$ (subsumer ledger) — the set of basic concepts $A$ is known to be subsumed by; $B \in S(A)$ means $A \sqsubseteq B$ . Seeded with $\{A, \top\}$ .
$R(r)$ (edge ledger) — the set of concept-pairs $(A, B)$ with $A \sqsubseteq \exists r.B$ ; seeded empty.
Completion / saturation — firing the rules until a full pass adds nothing; the least fixpoint of a monotone operator, the same shape as $T_P$ .
CR1–CR4 — the four rules matching normal forms NF1–NF4: subsumption transitivity, conjunction, existential introduction (writes an edge), existential elimination (reads an edge, writes a subsumer).
CR⊥ (the bottom rule) — propagates ⊥ backward across a role edge: an edge into an impossible concept makes the source impossible too.
CRχ (the role-chain rule) — composes two edges through $r \circ s \sqsubseteq t$ .
Unsatisfiable concept — one with $\bot \in S(A)$ ; provably empty in every model (TenuredStudent, TenuredStudentAdvisor).
Fixpoint / while changed — the executable form of $T(X) = X$ : a whole round adding nothing certifies saturation is complete.

Where this leads

We have an engine that halts, is cheap, and gets the academic world right — but "right on one example" is a promise, not a proof. The next chapter, Soundness and Completeness, makes good on the promise: it proves that these rules derive only true subsumptions (soundness, by showing every rule preserves entailment) and all true subsumptions (completeness, by building a canonical model from the saturated ledgers in which anything the rules failed to derive is demonstrably false). That pair of proofs is what upgrades the completion algorithm from "a loop that worked here" to "a decision procedure you can trust" — the guarantee that makes a reasoner worth calling a reasoner.

What this chapter covers​

The two tables: S(A) and R(r)​

The six rules, keyed to the four normal forms​

The engine: fire every rule until nothing changes​

A derivation by hand: the roles re-derive Professor ⊑ Researcher​

The bottom rule earning its keep​

The fixpoint, measured​

The unsolved part​

Why it matters​

Key terms​

Where this leads​