The Running Example: One Knowledge Base, Five Volumes

📍 Where we are: Part IV · The Neuro-Symbolic Idea — Chapter 14. The Kautz Taxonomy just sorted every way of wiring a neural learner to a symbolic reasoner into six named patterns; this chapter introduces the one small world on which all six patterns — and all five volumes of this series — get measured.

We have used the same tiny academic world as a proving ground all volume long, but always in fragments: a rule here, a query there, a scatter of embedded points at the end. This chapter puts the whole thing on the table at once — every individual, every base fact, every rule — and then shows the deeper structure that has been hiding in plain sight: an ontology folded into the rules, questions that hop across several links, and two dimensions of annotation the later volumes will switch on. The payoff is not the world itself, which is deliberately small. It is that one world, re-read through five different lenses, is what lets the whole series compare its methods honestly. And because the world is small, we can do here what the rest of this book insists on: not merely state that twenty-three facts grow into forty-seven, but derive it, wave by wave, and check every derived atom against the number the companion code actually prints.

The simple version

Imagine one small town that five documentary crews each film. The first crew films the paperwork — who is officially what, and what the rules say follows. The second draws the town's family tree of categories. The third makes a map where friends live close together. The fourth follows two-step questions, like "who is my grandparent's neighbour." The fifth asks how sure anyone is about anything. Five very different films — but the same town, the same people, the same streets. Because the town never changes, you can lay the films side by side and see exactly what each way of looking adds. This chapter is that town.

What this chapter covers

• The whole knowledge base at once — the individuals, the seven base predicates, and the seven Horn rules from kb.py, and a hand-worked derivation of the 47-atom model, wave by wave.
• The immediate-consequence operator — the one function whose repeated application is forward chaining, defined precisely and traced through the sizes [23, 41, 47, 47].
• The ontology hiding in the rules — the implicit class hierarchy professor ⊑ researcher ⊑ person and the role chain advises ∘ advises ⊑ grandAdvisor, a preview of Volume 2's description logic, with every symbol decoded.
• Questions that hop — multi-hop queries like "who does alice grand-advise," answered by SLD resolution with a proof tree read link by link, a preview of Volume 4's complex query answering.
• The annotations not yet written — employment intervals over affiliations (temporal) and confidence weights on citations (uncertain), with the transitive-citation probability worked out, previews of Volumes 2 and 5.
• Five lenses on one world — a single table that reads the same knowledge base as logic, ontology, geometry, differentiable queries, and calibrated trust, plus a from-scratch TransE whose loss we watch fall.
• Why one example matters — coherence and comparability across the series, and the shared setting where the SATORI capstone measures its joint claims.

One knowledge base, laid out whole

The cast of the academic world is fixed and small. The companion file kb.py names every individual up front, on lines 32–35:

PEOPLE = ["alice", "bob", "carol", "dave", "erin"]
PAPERS = ["p1", "p2", "p3"]
INSTITUTIONS = ["mit", "cmu"]
TOPICS = ["logic", "ml", "nesy"]

Thirteen individuals in four kinds: five people, three papers, two institutions, three topics. Every one of them is a constant: a fixed name that stands for one specific thing. The file's is_var function (lines 25–28) draws the only line that matters for the reasoning to come: a string that starts with an uppercase letter ("X", "Who") is a variable, a placeholder that can stand for any individual; everything lowercase ("alice", "p1") is a constant, standing for itself. Hold that convention: it is the entire difference between a fact and a rule.

On top of the individuals the file asserts base facts — what kb.py labels the ABox (assertion box): the things we state directly rather than derive.

# --- Base facts (the ABox: what we assert directly) ------------------------
# Class memberships. alice and bob are professors; carol/dave/erin are students.
FACTS: list[tuple] = [
    ("professor", "alice"),
    ("professor", "bob"),
    ("student", "carol"),
    ("student", "dave"),
    ("student", "erin"),
    # Advising (a professor advises a student). Note the chain alice→bob→carol,
    # which lets a *grandAdvisor* be derived by composing advises with itself.
    ("advises", "alice", "bob"),
    ("advises", "bob", "carol"),
    ("advises", "bob", "dave"),
    ("advises", "carol", "erin"),

Seven predicates are asserted in all: two that label what someone is — professor and student — and five that link two things — advises, authored, cites, affiliated, and about. The number of arguments a predicate takes is its arity: professor is unary (arity 1), advises is binary (arity 2). The file continues past the excerpt above with authorship (authored), a citation chain (cites, running p3 → p2 → p1), affiliations (affiliated, each person at exactly one institution), and subjects (about). Counting every line in the FACTS list (lines 39–69), that is exactly 23 base facts. Each one is an atom: a predicate followed by its arguments, written as a plain tuple like ("advises", "alice", "bob"). An atom with no variables in it, like every one of these, is called ground.

Then come the rules — kb.py's intensional predicates, the ones computed rather than stated (lines 73–89). Every rule is a Horn rule: a single positive conclusion (the head) that holds whenever a conjunction of conditions (the body) all hold. A fact, in this light, is just a rule with an empty body.

# --- Rules (the intensional/derived predicates) ----------------------------
# Every rule is Horn: one positive head, a conjunction of positive body atoms.
RULES: list[tuple] = [
    # A professor or a student is a researcher; a researcher is a person.
    (("researcher", "X"), [("professor", "X")]),
    (("researcher", "X"), [("student", "X")]),
    (("person", "X"), [("researcher", "X")]),
    # Grand-advising = advising composed with advising (a role chain).
    (("grandAdvisor", "X", "Z"), [("advises", "X", "Y"), ("advises", "Y", "Z")]),
    # Colleagues share an institution (the X != Y guard is applied by the engine
    # via the built-in `neq` check; see forward_chain.py / sld.py).
    (("colleague", "X", "Y"),
     [("affiliated", "X", "I"), ("affiliated", "Y", "I"), ("neq", "X", "Y")]),
    # Transitive closure of citation — the rule that *needs* a fixpoint, because
    # its own head feeds its own body.
    (("citesTransitively", "A", "B"), [("cites", "A", "B")]),
    (("citesTransitively", "A", "C"),
     [("cites", "A", "B"), ("citesTransitively", "B", "C")]),
]

Seven rules define five derived predicates: researcher, person, grandAdvisor, colleague, and citesTransitively. Read each rule right to left: (("researcher", "X"), [("professor", "X")]) says "for any X, if professor(X) holds then researcher(X) holds." The last two rules are the subtle ones. colleague carries a built-in neq (not-equal) guard so that a person is never counted as their own colleague, and citesTransitively feeds its own head back into its own body, so it settles only once you compute a fixpoint — a set that stops changing when the rules are applied again.

The immediate-consequence operator, and the meaning of the program

To say precisely what those rules mean, we need one function. Write $P$ for the program (the facts together with the rules) and $I$ for a set of ground atoms we currently believe (an interpretation). The immediate-consequence operator $T_P$ takes $I$ and returns $I$ together with every head we can fire in a single step:

$$T_P(I) \;=\; I \,\cup\, \bigl\{\, h\sigma \;:\; (h \leftarrow b_1 \wedge \cdots \wedge b_m)\in P,\ \ \text{every } b_i\sigma \text{ is satisfied in } I \,\bigr\}.$$

Every symbol here earns its place. The union sign $\cup$ means "put both sets together." The braces $\{\,\cdot : \cdot\,\}$ are set-builder notation, read "the set of all things of this form such that this condition holds." The arrow $h \leftarrow b_1 \wedge \cdots \wedge b_m$ is one rule, its head $h$ on the left and its body atoms $b_1,\ldots,b_m$ joined by $\wedge$ ("and") on the right; the subscript index $i$ in $b_i$ just numbers the body atoms from $1$ to $m$. The Greek letter $\sigma$ (sigma) is a substitution, a lookup table that replaces each variable by a constant, and $h\sigma$ means "apply that replacement to $h$." The membership sign $\in$ reads "is an element of." What it means for a body atom $b_i\sigma$ to be satisfied in $I$ splits into two cases, exactly as the code does. An ordinary atom is satisfied when it is literally present: $b_i\sigma \in I$. A built-in guard — our only one is $\text{neq}(s, t)$ ("not equal") — is never stored in $I$ at all; it is satisfied when its two arguments $s\sigma$ and $t\sigma$ have become distinct constants. That second clause is not decoration: the colleague rule's body ends in neq(X, Y), so without it the rule could never fire and the eight colleague atoms we count below could never be derived. So the whole line says, in plain words: keep everything already in $I$, and add the head of any rule whose body atoms, after some consistent renaming of variables to constants, are all satisfied in $I$ — each ordinary atom present as a fact, each guard checking out true on its now-ground arguments. That is exactly one sweep of forward chaining.

This operator is not a metaphor; it is a function in the code. In forward_chain.py, t_p (lines 42–49) loops over every rule, asks _match_body (lines 19–39) for every substitution that makes the body true in the current facts, and adds apply_sub(head, sub) — precisely $h\sigma$ — to the output. The neq guard is handled inside _match_body (lines 30–34): it is not looked up as a fact but checked, succeeding only when its two arguments have become different constants.

The meaning of the whole program is what you reach by applying $T_P$ over and over, starting from the base facts. Define a chain of interpretations $I_0, I_1, I_2, \ldots$ by

$$I_0 = \text{FACTS}, \qquad I_{k+1} = T_P(I_k).$$

Because each step only adds atoms ($I_k \subseteq I_{k+1}$, where $\subseteq$ reads "is a subset of, or equal to") and there are only finitely many ground atoms you could ever build from thirteen constants and twelve predicates (the seven asserted ones plus the five derived — researcher, person, grandAdvisor, colleague, citesTransitively — that the rules introduce), the chain cannot grow forever. It must hit a step where nothing new appears, $I_{k+1} = I_k$. That stable set is the least fixpoint $\mathrm{lfp}(T_P)$, and it is exactly the least Herbrand model: the one canonical set of true atoms the program entails. In least_fixpoint (lines 52–64) this is the while True loop, and the halting test is the single line if nxt == current (line 61): stop when a sweep changed nothing.

Deriving the model wave by wave

Now we run that operator by hand and watch the sizes it prints, [23, 41, 47, 47], appear one at a time. This is the chapter's central worked trace: not a claim that the facts "grow into 47 atoms," but a ledger of which atoms enter on which sweep, and why.

Wave 0. $I_0$ is the 23 base facts. Size $= 23$.

Wave 1 applies $T_P$ to those 23 facts. We check each rule against $I_0$:

Rule (head ← body)	Bodies satisfied in $I_0$	New heads added
researcher(X) ← professor(X)	professor(alice), professor(bob)	researcher(alice), researcher(bob)
researcher(X) ← student(X)	student(carol), student(dave), student(erin)	researcher(carol), researcher(dave), researcher(erin)
person(X) ← researcher(X)	none — no researcher atom exists yet	—
grandAdvisor(X,Z) ← advises(X,Y) ∧ advises(Y,Z)	alice→bob→carol, alice→bob→dave, bob→carol→erin	grandAdvisor(alice,carol), grandAdvisor(alice,dave), grandAdvisor(bob,erin)
colleague(X,Y) ← affiliated(X,I) ∧ affiliated(Y,I) ∧ neq(X,Y)	mit: $\{\text{alice}, \text{bob}\}$; cmu: $\{\text{carol}, \text{dave}, \text{erin}\}$	8 ordered pairs (see below)
citesTransitively(A,B) ← cites(A,B)	cites(p2,p1), cites(p3,p2)	citesTransitively(p2,p1), citesTransitively(p3,p2)
citesTransitively(A,C) ← cites(A,B) ∧ citesTransitively(B,C)	none — no citesTransitively atom exists yet	—

Two rules fire nothing in wave 1, and this is the whole reason the chain takes more than one step. person needs a researcher atom in its body, but the researchers are only being created this very sweep; they were not in $I_0$. The recursive citation rule needs a citesTransitively atom in its body, and none existed in $I_0$ either. Both must wait for the next wave.

The colleague count deserves its own arithmetic, because the neq guard makes it exact. For a set $S$ of people sharing one institution, the rule fires once for each ordered pair of distinct people, and the number of such pairs is $|S|\,(|S|-1)$ (the vertical bars $|S|$ mean "the number of elements in $S$"). At mit, $S = \{\text{alice}, \text{bob}\}$ gives $2 \times 1 = 2$ pairs; at cmu, $S = \{\text{carol}, \text{dave}, \text{erin}\}$ gives $3 \times 2 = 6$ pairs. Total $2 + 6 = 8$, and the eight ordered pairs are (alice,bob), (bob,alice), (carol,dave), (dave,carol), (carol,erin), (erin,carol), (dave,erin), (erin,dave). The neq guard is what removes the would-be self-pairs like (alice,alice), and it is why colleague is symmetric but never reflexive.

Adding wave 1's new atoms: 5 researchers $+$ 3 grandAdvisors $+$ 8 colleagues $+$ 2 citesTransitively $= 18$. So $|I_1| = 23 + 18 = 41$, the second number the code prints.

Wave 2 applies $T_P$ to those 41 atoms. Every rule that fired in wave 1 fires again and re-derives the same heads (adding nothing new), but now the two stalled rules finally have their bodies:

Rule	Bodies newly satisfied in $I_1$	New heads added
person(X) ← researcher(X)	researcher(alice), …, researcher(erin)	person(alice), person(bob), person(carol), person(dave), person(erin)
citesTransitively(A,C) ← cites(A,B) ∧ citesTransitively(B,C)	cites(p3,p2) ∧ citesTransitively(p2,p1)	citesTransitively(p3,p1)

That is 5 person atoms plus the single transitive edge citesTransitively(p3,p1), which is the one atom nobody could shortcut: it exists only because a derived atom, citesTransitively(p2,p1), was fed back into the rule that produced it. New atoms $= 6$, so $|I_2| = 41 + 6 = 47$, the third printed number.

Wave 3 applies $T_P$ to the 47 atoms and produces no head that is not already present — in particular citesTransitively(p3,p1) is re-derived, not newly found. So $I_3 = I_2$, the equality test on line 61 succeeds, and iteration stops. The printed size list is $|I_0|, |I_1|, |I_2|, |I_3| = [23, 41, 47, 47]$, and the reported round count is $\text{len(sizes)} - 1 = 3$. Running the file confirms the ledger exactly:

least fixpoint reached in 3 rounds; sizes per round: [23, 41, 47, 47]
47 atoms total, 24 derived.
   ('citesTransitively', 'p2', 'p1')
   ('citesTransitively', 'p3', 'p1')
   ('citesTransitively', 'p3', 'p2')

The 24 derived atoms split exactly as our trace predicts: 5 researcher, 5 person, 3 grandAdvisor, 8 colleague, and 3 citesTransitively, summing to $5+5+3+8+3 = 24$, and $23 + 24 = 47$. That 47-atom model is the fixed object every later volume re-reads. Nothing about it is asserted by hand beyond the original 23 lines; the other 24 atoms are forced by the rules, and we have now watched each one arrive.

The ontology hiding in the rules

Look again at the first three rules. They are not really about individuals; they are about kinds. Every professor is a researcher, every student is a researcher, and every researcher is a person. Written in the notation of description logic — where the subsumption symbol ⊑ reads "is a kind of" (more precisely, "every instance of the left-hand class is also an instance of the right-hand class") — those rules are a class hierarchy:

$$\text{professor} \sqsubseteq \text{researcher} \sqsubseteq \text{person},$$

with student ⊑ researcher as its sibling branch. Subsumption chains, so from professor ⊑ researcher and researcher ⊑ person we may conclude professor ⊑ person, and therefore that professor(alice) entails person(alice). That is not a new axiom; it is the same conclusion forward chaining reached by firing rule R1 (professor to researcher) in wave 1 and rule R3 (researcher to person) in wave 2. The one-wave gap we traced above is the operational shadow of a two-link subsumption chain.

The grandAdvisor rule says something a plain hierarchy cannot: it composes a relation with itself. If X advises Y and Y advises Z, then X grand-advises Z — a role chain, written

$$\text{advises} \circ \text{advises} \sqsubseteq \text{grandAdvisor},$$

where the ring operator ∘ reads "composed with," or "followed by": travel one advises edge and then another, and you are allowed to call the two-step journey a grandAdvisor edge. The class hierarchy sits comfortably inside EL, the lightweight description logic whose characteristic constructors are conjunction (⊓, read "and," the class of things in both classes at once) and existential restriction (∃r.C, read "has some r-relationship to a member of class C"; the ∃ is "there exists" and the dot separates the role r from the class C). The role chain reaches past plain EL: composing a role with itself is a complex role inclusion, part of the extension EL++, which is exactly why OWL 2 EL — the ontology-language profile built on EL++ — supports both class hierarchies and role chains. Together the hierarchy and the chain make our facts-and-rules file also an implicit TBox (terminology box: the schema-level axioms about kinds, as opposed to the ABox's assertions about individuals) sitting quietly above its ABox [1]. That is precisely how kb.py describes itself — an EL++ ontology waiting for Volume 2. Volume 2 makes the TBox explicit and hands it to a reasoner, a program that classifies the world — deriving the same person and grandAdvisor atoms forward chaining found, but now as logical consequences of an ontology rather than of a Datalog program. Same conclusions, a richer justification.

Questions that hop

Forward chaining derives everything; a query engine derives just what you asked. The backward-chaining prover in sld.py answers queries: give it a goal with a variable and it enumerates every binding that makes the goal provable. Where forward chaining runs $T_P$ blindly outward, backward chaining starts from the goal and works inward, asking at each step "which rule could conclude this, and what would its body then require?" The engine is _solve (lines 37–60): to prove a goal, it renames a rule's variables afresh (line 53, so reusing the recursive citation rule cannot capture variables), tries to unify the rule's head with the goal (line 54, meaning it finds a substitution making the two identical), and, on success, recursively proves the body atoms under that substitution. A base fact is stored as a rule with an empty body, so it proves immediately with no children.

Asking "who does alice grand-advise?" is one such query, and answering it must hop twice — once along advises from alice to bob, again along advises from bob to each of bob's students:

>>> from sld import answers
>>> answers(("grandAdvisor", "alice", "Who"))
[('grandAdvisor', 'alice', 'carol'), ('grandAdvisor', 'alice', 'dave')]

Trace what _solve does with it. The goal grandAdvisor(alice, Who) unifies with the head grandAdvisor(X, Z) under the substitution $\{X \mapsto \text{alice},\, Z \mapsto \text{Who}\}$ (the maplet $\mapsto$ reads "is replaced by"). The body then demands advises(alice, Y) ∧ advises(Y, Z). Proving advises(alice, Y) against the facts binds $Y \mapsto \text{bob}$, the only match. That leaves advises(bob, Z), which matches two facts, binding $Z \mapsto \text{carol}$ and $Z \mapsto \text{dave}$. Each success is turned into a ground answer by apply_sub(goal, sub) (line 92), and answers collects and sorts them, yielding exactly grandAdvisor(alice, carol) and grandAdvisor(alice, dave). These are the same two atoms forward chaining produced in wave 1 — the two engines agree, as a sound and complete Datalog reasoner must, differing only in whether they compute everything (forward) or just the goal (backward).

Because SLD resolution (the backward-chaining strategy behind Prolog) returns a proof tree, each answer is auditable, not merely asserted — you can read off exactly which facts were chained. The Proof class (lines 19–34) holds the goal proved plus the sub-proofs of the body that established it, and its render method prints the tree indented:

proof of grandAdvisor(alice, carol):
  grandAdvisor(alice, carol)
    advises(alice, bob)
    advises(bob, carol)
colleagues of alice: [('colleague', 'alice', 'bob')]

The root is the conclusion; its two leaves are the two base facts that discharge the role chain, one hop each. A two-hop query is the simplest multi-hop query: a question whose answer is not stored anywhere but must be composed by following several edges in turn. Volume 4 asks these same questions of a learned model, answering them by geometry when a proof is unavailable — an approach popularized by box-embedding query engines such as Query2box, which answer multi-hop existential queries directly in vector space [2]. The query is identical; only the machinery that answers it changes, from an auditable proof tree to a point in a learned space.

The annotations not yet written

The kb.py facts are crisp and timeless: affiliated(bob, mit) is simply true, full stop. The real academic world is neither crisp nor timeless, and two latent annotations ride quietly on the very same individuals, waiting for later volumes to switch them on.

The first is time. Read affiliated as an employment interval rather than a bare edge — bob at mit from 2019 to 2024 — and every colleague query acquires a "when": two people are colleagues only during the years their intervals overlap. If alice is at mit over [2015, 2020] and bob over [2019, 2024], they are colleagues only across the overlap [2019, 2020], and the eight-pair colleague count we derived above becomes a set of time-stamped pairs, some of which may be empty. Layering intervals onto the relations is a temporal extension of the ontology, the kind of richer axiom Volume 2 takes up once the plain TBox is in hand.

The second is uncertainty. Attach a confidence to each cites edge — say p2 cites p1 with weight 0.9 and p3 cites p2 with weight 0.6 — and citesTransitively stops being a crisp closure and becomes a chain of probabilities whose product decays with every hop. The one hard-won transitive edge from our trace, citesTransitively(p3, p1), was built by chaining p3 → p2 → p1; under the standard independence assumption its confidence is the product along the path,

$$\Pr[\text{p3} \to \text{p1}] \;=\; 0.6 \times 0.9 \;=\; 0.54,$$

already below either link that produced it, and falling further with every extra hop. Calibrating those weights, so that a stated 0.9 is right about nine times in ten, is exactly Volume 5's concern with trust. Neither annotation changes the cast; both change what a question means over it. That is the quiet advantage of one shared world: you can add whole new dimensions without rebuilding the individuals underneath.

Five lenses on one world

The same knowledge base, read five ways, is the spine of the whole series. Each volume keeps the individuals and edges fixed and swaps only the representation — which is what makes the volumes commensurable at all [3].

One academic world at the hub, read through five lenses in turn — logic and learning, ontology and reasoner, embeddings, differentiable query answering, and trust — so that across all five volumes only the method changes and the world stays fixed. Original diagram by the authors, created with AI assistance.

Volume	Lens	What it reads in the academic world
Volume 1 — Foundations	Logic and learning	Forward-chain the 23 facts to 47 atoms, prove goals by SLD, and place the symbols with a from-scratch TransE
Volume 2 — Ontology and reasoner	Description logic	The same facts as an EL++ TBox plus ABox — professor ⊑ researcher ⊑ person, advises ∘ advises ⊑ grandAdvisor — classified by a reasoner
Volume 3 — Embeddings	Geometry at scale	The 13 entities and 5 relations learned as region embeddings (boxes, balls), so subsumption becomes containment
Volume 4 — Differentiable query answering	Complex queries in vector space	Multi-hop questions like "who does alice grand-advise" answered by geometry, not only by proof
Volume 5 — Trust and the frontier	Calibration and proof	Uncertain citations and faithful proof traces, where the SATORI capstone measures joint claims

From proof to geometry: a TransE you can watch learn

The embeddings.py companion already lets you feel the jump from lens one (logic) to lens three (geometry) on this exact world. It trains a two-dimensional TransE model, whose one idea is that a relation is a translation: place every entity and every relation as a vector, and ask that for a true triple $(h, r, t)$ — head, relation, tail — the head plus the relation land near the tail, $e_h + e_r \approx e_t$ (the symbol ≈ reads "is approximately equal to," and $e_x \in \mathbb{R}^2$ is the two-number vector the model learns for symbol $x$). The plausibility of a triple is then just how badly that translation misses, measured by the score

$$s(h, r, t) \;=\; \lVert e_h + e_r - e_t \rVert \;=\; \sqrt{\textstyle\sum_{i=1}^{2} \bigl(e_{h,i} + e_{r,i} - e_{t,i}\bigr)^2},$$

where the double bars $\lVert \cdot \rVert$ denote the length of a vector (its Euclidean norm), $\Sigma$ sums over the $d = 2$ coordinates indexed by $i$, and lower means more plausible. This is score in the file (lines 101–104), built on the squared-distance helper _dist2 (lines 32–33). The subtlety worth naming: _dist2 returns the squared distance $\lVert\cdot\rVert^2$, which is what the training loss uses, while score takes the square root to report an honest distance; both rank triples the same way, since square root is increasing.

Training pushes true triples below corrupted ones by a margin-ranking loss. For a true triple and a corrupted copy $(h, r, t')$ made by swapping the tail for a random wrong entity, the loss is

$$\ell \;=\; \max\!\bigl(0,\; \gamma + d(e_h{+}e_r,\, e_t) - d(e_h{+}e_r,\, e_{t'})\bigr),$$

with $d(a,b) = \lVert a - b\rVert^2$ the squared distance and the margin $\gamma = 1.0$ (margin in the file). Read it as a demand: the true tail must be closer than the false tail by at least $\gamma$, or you pay. This is eval_loss (lines 67–72) and the training check on line 87 (if margin + d_pos - d_neg <= 0: continue skips a triple already ranked correctly). When the loss is active, its gradient with respect to a coordinate of the head vector is, by differentiating $d$ (the symbol $\partial$ is a partial derivative, introduced in the gradient-descent chapter: the slope of the loss $\ell$ along one coordinate with all the others held fixed),

$$\frac{\partial \ell}{\partial e_{h,i}} \;=\; 2\bigl(e_{h,i}+e_{r,i}-e_{t,i}\bigr) - 2\bigl(e_{h,i}+e_{r,i}-e_{t',i}\bigr),$$

which is line 93 verbatim: gh = 2 * diff_pos - 2 * diff_neg, with diff_pos and diff_neg the two parenthesised differences. The four update lines that follow (lines 94–97) step the head, relation, true tail, and corrupt tail along their gradients — the same $\theta \leftarrow \theta - \eta\,\nabla_\theta L$ walk downhill derived in the gradient-descent chapter, here applied one triple at a time. Watching the mean hinge loss fall over training makes the descent visible:

epoch	0	1	5	20	100	500	2000
hinge loss	1.522	1.319	0.802	0.224	0.132	0.062	0.089

The loss drops by more than an order of magnitude within a hundred epochs and then hovers near zero; the tiny rise from 0.062 at epoch 500 to 0.089 at epoch 2000 is the residual jitter of stochastic gradient descent on vectors that are renormalised to the unit circle each sweep, not a failure to learn. After the full run the geometry cleanly separates truth from fiction:

mean score  true triples = 1.609   corrupted = 2.737
score advises(alice, bob)  = 0.399  (true)
score advises(alice, erin) = 0.929  (false)

The learned map scores the real edge advises(alice, bob) at 0.399 and the invented advises(alice, erin) at 0.929 — more than twice as far — and across all triples the true set averages 1.609 against the corrupted set's 2.737. Nobody ever told the model that advises(alice, erin) is false; the gap is a consequence of fitting the true edges, the same way the 24 derived atoms were a consequence of the rules. That is the same world the logic engine forward-chained, now answering a question logic refused to touch: not "is this provable?" but "how plausible is this?"

Why one shared example matters

Reusing a single example is not a stylistic tic; it is what makes the series comparable. When Volume 1 forward-chains 47 atoms, Volume 3 embeds the same 13 entities, and Volume 4 answers the very same grand-advising query, a reader can hold the three methods against one another because only the method changed — the world did not. The small academic world is the control variable of the whole series: pin the data down to the last atom and any difference you see afterward has to be a difference in the method. A knowledge graph is exactly the right shared substrate for this, since its nodes-and-edges shape is the common denominator that logic, ontology, embeddings, and query engines all already read [3].

That control variable is also where the series' capstone earns its keep. SATORI, the joint system Volume 5 builds toward, measures its claims on this very knowledge base: does adding the ontology improve a learned model's answers to multi-hop queries, and does it do so without wrecking the model's calibration? Because the setting never moves, that question has a clean answer instead of a confound — any change in the score is a change in the method, not in the data. The 0.399-versus-0.929 gap we just watched TransE learn is precisely the kind of quantity SATORI will try to widen with an ontology while keeping its confidences honest.

The unsolved part

Here is the honest gap the series is aimed at. Each lens has a mature public benchmark of its own: ontology reasoners are graded on standard OWL test suites, embedding models on link-prediction splits, and complex-query systems on Query2box-style multi-hop datasets [2]. But no public benchmark asks all of them at once. None hands a system an ontology and a bank of multi-hop queries and a demand for calibrated uncertainty, then scores whether one model can honour all three together — hierarchy respected, hops composed correctly, and confidences that mean what they say. Every existing benchmark isolates one lens and quietly assumes the others away. Our academic world is a hand-built stand-in for the joint benchmark that does not yet exist — which is precisely the missing piece the final volume names, and the reason the frontier still feels unsettled even though each individual capability is, on its own, solved.

Why it matters

Neuro-symbolic AI is, at bottom, the claim that two ways of representing the same world — exact symbolic logic and approximate learned geometry — can be made to cooperate rather than compete. That is a strong claim, and strong claims need something concrete to be checked against. Every chapter ahead that promises "logic gives guarantees, learning gives coverage, and the fusion gives both" is a promise you can now weigh against a specific 47-atom model whose every derived fact you have watched arrive, wave by wave, and against a specific learned geometry whose loss you have watched fall. When a later volume reports that an ontology-guided model answered a query the plain embedding missed, you will already know the query, the ontology, and the embedding — because all three live in this one small town. That is what turns a slogan about cooperation into an experiment with an answer.

Key terms

• Running example (the academic world) — the single knowledge base of 13 individuals, 23 base facts, and 7 rules, threaded through all five volumes as a fixed control variable.
• ABox / TBox — the assertion box (facts about individuals, e.g. professor(alice)) and the terminology box (axioms about kinds, e.g. professor ⊑ researcher); kb.py's FACTS are the ABox, its RULES imply a TBox.
• Atom / ground / arity — an atom is a predicate applied to arguments, like ("advises", "alice", "bob"); it is ground when it contains no variables; a predicate's arity is how many arguments it takes.
• Horn rule — a rule with one positive head and a conjunction of positive body conditions; a fact is a Horn rule with an empty body.
• Immediate-consequence operator $T_P$ — the function that adds every rule head whose body already holds; forward chaining is $T_P$ applied repeatedly until nothing changes.
• Least fixpoint — the smallest set of atoms stable under $T_P$; here reached in three waves with sizes [23, 41, 47, 47] and equal to the 47-atom model.
• Class hierarchy — a chain of subsumptions such as professor ⊑ researcher ⊑ person, read with ⊑ as "is a kind of."
• Role chain — a relation composed with itself or another, such as advises ∘ advises ⊑ grandAdvisor, read with ∘ as "followed by"; formally a complex role inclusion.
• EL / EL++ — EL is the lightweight description logic whose core constructors are conjunction (⊓) and existential restriction (∃r.C); EL++ is its extension, adding features such as complex role inclusions (role chains), and is the basis of OWL 2 EL — together the logic our rules implicitly inhabit.
• SLD resolution / proof tree — the backward-chaining strategy (behind Prolog) that proves a goal by unifying it with rule heads and recursively proving bodies, returning an auditable proof tree.
• Multi-hop query — a question whose answer is composed by following several edges in turn, such as "who does alice grand-advise."
• TransE / margin-ranking loss — the embedding model that treats a relation as a translation ($e_h + e_r \approx e_t$) and trains true triples to score below corrupted ones by a margin.
• Region embedding — Volume 3's geometry that represents a class as a box or ball, so a hierarchy becomes literal containment.
• Calibration — the property that a stated confidence matches reality, so an edge asserted at 0.9 is right about nine times in ten; Volume 5's concern.
• SATORI capstone — the joint neuro-symbolic system the series builds toward, measured on this same knowledge base.

Where this leads

We now have the whole world in one place: its individuals, its 23 facts, its 7 rules, the 47-atom model they grow into wave by wave, the ontology folded into those rules, the multi-hop questions they answer with auditable proofs, and the temporal and uncertain layers still to come — all ready to be re-read through five lenses. The next and final chapter of this volume, The Honest Verdict, steps back from the machinery to ask the blunt question the whole field must face: after everything logic and learning each do well, what does neuro-symbolic AI actually deliver today, what does it only promise, and where — on exactly this shared world — does the real frontier still lie.