Preface — Knowledge a Machine Can Trust

📍 Where we are: At the door of Volume 2 — Symbolic Reasoning. Volume 1 closed by weighing two halves of neuro-symbolic AI on one shared world: an exact-but-brittle symbolic half and a robust-but-opaque neural half. This volume takes the first half and builds it out in full — the ontologies, the logics, and the reasoners that turn "a fact you wrote down" into "a conclusion a machine can guarantee."

Welcome back. Volume 1 gave the symbolic half of neuro-symbolic AI in miniature: Horn rules, a forward-chaining engine, a proof you could read by eye. It worked, and its verdict was honest — the prover was sound and complete (it derives all and only what follows) but silent the instant a question stepped outside its rules. This volume asks what that silent, certain half becomes when you take it seriously: not a handful of hand-written rules, but a formal ontology; not one recursive predicate, but a whole description logic; not a toy loop, but the reasoners that classify ontologies with hundreds of thousands of classes. The world does not change — we re-read the very same academic knowledge base through a far sharper lens — and by the end you will know exactly what a symbol can promise a machine, and what it cannot.

The simple version

Imagine the most meticulous librarian alive. She never guesses. Every card in her catalog cross-references every other, so the moment you file one new rule — "a professor is a kind of researcher" — she silently re-shelves everything downstream, and can walk you card by card through why a book belongs where it does. Ask her a question she has no card for and she says, plainly, "not shown" — never a hunch. And if you ever hand her two cards that contradict each other, she stops, points at the exact pair, and refuses to pretend the shelf still makes sense. That librarian is symbolic reasoning. This volume is how she works: how knowledge gets written on the cards, what she is allowed to say, how she re-shelves everything without ever missing a case, and how fast she can do it on a library the size of medicine.

What this volume covers

Volume 2 is one continuous climb, from writing a single fact down to auditing everything symbols guarantee, in seven parts. Each part answers one question:

Part	Theme	The question it answers
I — Knowledge Representation	triples, graphs, RDF and OWL, the TBox/ABox split	How do you write knowledge down so a machine can hold and share it?
II — Description Logic	concepts, roles, individuals; the EL family; the OWL 2 profiles; complexity	What can you say — and what does saying it cost to reason about?
III — The EL Completion Algorithm	normalization, the completion rules CR1–CR4 and the bottom rule, soundness and completeness, consequence-based classification	How does a reasoner actually compute every entailment, provably and in full?
IV — Datalog and the Chase	rules, the $T_P$ operator and least fixpoint, existential rules, certain answers	How do rules and "something exists" answer queries over incomplete data?
V — Reasoners in Practice	ELK, CEL, RDFox, HermiT, Konclude; the LUBM, OWL2Bench, and ORE benchmarks	Do these algorithms actually run at real-world scale?
VI — Annotated and Temporal Logic	provenance semirings, confidence lattices, Allen's interval algebra, open-world and repair	What changes when a fact carries a source, a confidence, or a time?
VII — The Verdict	what symbols guarantee, and what stays out of reach	What did all of this machinery genuinely buy you?

Who this volume is for

This is written for a reader one notch past Volume 1 — a sophomore ramping toward a junior. It assumes you have met sets, relations, first-order logic, and the least fixpoint of a monotone operator, but it re-teaches each on the spot the first time it matters, so any gap is a pause, not a wall. Nothing arrives as a black box: when we need a reasoner, we build one from scratch in pure Python, and only then cross-check it against a real engine — owlready2 driving the ELK and HermiT reasoners — so you see both the mechanism and the proof it is right.

The thesis: knowledge a machine can trust

Here is the conviction the volume turns on. Symbolic reasoning buys you correctness you can trust and explain, on knowledge you must write down and keep consistent — and both clauses are load-bearing. The reward is real: when the reasoner reports $\text{Professor} \sqsubseteq \text{Person}$ (read "every professor is necessarily a person"), it is not a strong hunch but a theorem — true in every model of the ontology — and it can hand you the derivation that proves it. Better still, deciding such subsumptions is not merely possible but tractable in the right logic: for the EL family, classification runs in polynomial time, which is exactly why the librarian can re-shelve a library the size of medicine and finish.

The price is just as real. A reasoner reads your model of the world, not the world: it reasons only over axioms someone authored, it treats an unknown fact as merely unproven rather than false (the open-world assumption), and the instant two axioms contradict, classical entailment collapses into deriving everything. That is the exact-but-brittle half of Volume 1's verdict, now developed in full.

The running example, re-read as an ontology

We keep Volume 1's world down to the last fact, and change only the lens. The same five people, three papers, two institutions, and topics are re-read as an EL++ ontology: 10 named concepts, 6 roles, 14 TBox axioms; ABox: 13 concept assertions, 18 role assertions over 13 individuals. The schema becomes a TBox (terminological box) of concept and role axioms; the ground data becomes an ABox (assertional box) built directly from Volume 1's facts, so it is provably the same world.

Four pieces of structure carry the whole volume. The concept hierarchy $\text{Professor} \sqsubseteq \text{Researcher} \sqsubseteq \text{Person}$ is the skeleton every classifier must recover. The role chain $\text{advises} \circ \text{advises} \sqsubseteq \text{grandAdvisor}$ says advising your advisee's advisor makes you their grand-advisor — one axiom that only description logic, not plain hierarchy, can express. The disjointness $\text{Professor} \sqcap \text{Student} \sqsubseteq \bot$ declares that nobody is both, which gives the bottom rule its work. And two concepts — TenuredStudent and TenuredStudentAdvisor — are deliberately built to be unsatisfiable: a correct reasoner must catch that they can have no instances at all. Run the from-scratch completer and it saturates the 23 stated subsumptions to 39 in three rounds, reads off exactly 8 subsumptions among the named concepts, flags those 2 unsatisfiable concepts, and a 13-check ledger certifies every number.

One academic world re-read as an EL++ ontology — a TBox hierarchy with a role chain, a disjointness, and two unsatisfiable concepts — classified by a polynomial-time saturation that matches a real reasoner, the seven-part climb of the volume laid out beneath. Original diagram by the authors, created with AI assistance.

The one loop underneath

If you carry one idea from Volume 1 into this one, carry the least fixpoint. Almost every reasoner ahead is the same loop you already proved correct: seed with the stated facts, apply a fixed set of monotone rules, and stop when a round adds nothing. Description-logic completion (Part III) is that loop firing entailment rules until the model saturates — the [23, 34, 39, 39] climb above is a Kleene ascent by another name. Datalog evaluation (Part IV) is literally the $T_P$ operator from Volume 1's fixpoint chapter. Even the chase, which handles rules that assert something exists, is the same climb — except now it can run forever, which is precisely why Part IV must draw the line between fragments that terminate and ones that merely stay decidable. Learn the loop once and you recognize it everywhere ahead.

Beyond true and false

Parts I through V live in a world of two answers: entailed, or not. Part VI is where knowledge grows a second dimension. Provenance semirings record where a derived fact came from, so a conclusion carries its own receipt. Annotated and confidence lattices attach how sure a fact is, combining degrees along a proof instead of collapsing them to a bare yes. Allen's interval algebra and temporal reasoning add when. And the open-world, inconsistency-tolerant methods add a machine's right to abstain — or to repair a contradiction rather than explode on it. These are the symbolic tools that meet the neural half's own talk of confidence and time head-on.

Where this leads

We have the shape of the whole climb now: one world, one loop, seven parts, and a clear promise — correctness a machine can trust, on knowledge it must be given. The foundation of all of it is the humblest object in the field: a single fact, written so a machine can hold it. The first chapter, Triples and Graphs, shows how every fact becomes a triple — subject, predicate, object — how a pile of triples is a labelled directed graph, and how the academic world turns into a knowledge graph of 13 individuals wired by 18 role edges you can traverse. Everything the librarian later guarantees is built on that one move, so we watch it happen slowly, on a world small enough to draw on a napkin.