Justifications: Minimal Proofs and Pinpointing

📍 Where we are: Part I · Proofs, Faithfulness, and Trust — Chapter 1. Volume 4's honest verdict conceded that differentiable logic buys learning, not trust; this volume opens by building trust's smallest unit, the checkable reason, on the crispest ground we have: the symbolic reasoner of Volume 2.

Volume 2's completion algorithm answers whether: run the fixpoint, read the saturated table, and the academic TBox (terminological box, the ontology's concept-level axioms) entails Professor ⊑ Researcher (every professor is a researcher; the symbol ⊑ is concept subsumption, Volume 2's workhorse). Volume 5 begins by demanding more. A clinician staring at a surprising subsumption in SNOMED CT (the Systematized Nomenclature of Medicine, Clinical Terms, the huge clinical ontology of Volume 2), an engineer whose ontology just classified a concept as unsatisfiable, a reviewer auditing a neuro-symbolic system's claimed derivation: all of them ask why, and none of them is helped by a fixpoint table with hundreds of entries. What they need is the justification: the exact, minimal set of axioms responsible for the conclusion, small enough to read, strong enough to force the entailment on its own, and tight enough that removing any one member breaks it. This chapter defines that object precisely, builds two algorithms for it (one justification by expand-contract, all justifications by a hitting-set tree descended from model-based diagnosis [1]), runs both against Volume 2's reasoner as a sealed black box, and then inverts the lens: the justifications of an unwanted entailment name exactly the axioms a repair must touch. Every claim is runnable, and on our 14-axiom world the enumeration is checked, exactly, against all 16,384 possible sub-ontologies.

The simple version

Imagine a verdict resting on a case file of fourteen documents. The judge does not want the whole file read back; she wants the minimal set of exhibits that still forces the verdict, such that withdrawing any single one would make the verdict no longer follow. That minimal exhibit set is a justification. A case can have several independent smoking guns: two different three-document bundles, either of which convicts on its own. And if you are the defense, the duality is exact: to overturn the verdict you must discredit at least one document out of every bundle, because any bundle left intact still convicts. Finding one bundle, finding all of them, and choosing the cheapest set of documents to attack: those are this chapter's three algorithms.

What this chapter covers

• Justification, defined and contrasted: a minimal entailing subset of the ontology, why it is the right unit of evidence, and how it differs from the derivations Volumes 1 and 2 already produce, on the grandAdvisor example.
• The black-box oracle discipline: the only primitive used anywhere is "does this axiom subset entail the conclusion?", implemented by re-running Volume 2's normalize-and-complete on the subset; why black-box pinpointing works for any reasoner and what glass-box methods buy instead.
• One justification by expand-contract: the contraction loop, the invariant it maintains, the proof that a single deletion pass yields a minimal set, and the drop-any-one certificate, all quoted with committed output.
• All justifications by Reiter's hitting-set tree: the tree decoded before it is formalized, its completeness argument worked in full, its pruning rules, and the exact-equality check against brute force over every one of the $2^{14}$ axiom subsets.
• Pinpointing as debugging: the justification of TenuredStudent ⊑ ⊥ read axiom by axiom, the theorem that repairs are exactly the hitting sets of the justification family, and the NP-hardness that puts a ceiling on minimum repair.
• The honest scale ledger: exponentially many justifications exist even in EL, and the field's levers (modules, glass-box tracing, proof-driven enumeration) each get a precise paragraph.

From derivations to evidence

Volume 1's forward chainer and Volume 2's completion algorithm both produce derivations: sequences of rule firings that end at the conclusion. A derivation is a perfectly good witness that an entailment holds. It is a poor unit of evidence, for two reasons. First, a derivation names rule applications, artifacts of one particular procedure; a different sound reasoner would emit a different derivation of the same fact, so the derivation tells you about the algorithm as much as about the knowledge. Second, and worse, nothing about a derivation is minimal: the forward chainer of Volume 1 saturates the whole knowledge base, so the closure that contains grandAdvisor(alice, carol) also contains every colleague fact and the entire transitive citation closure, none of which had anything to do with it.

Look at that example closely, because it already contains the whole idea. In Volume 1's kb.py, the fact grandAdvisor(alice, carol) is derived from exactly three statements: the two facts advises(alice, bob) and advises(bob, carol), and the one rule grandAdvisor(X, Z) :- advises(X, Y), advises(Y, Z). That three-element set is the evidence. It entails the conclusion by itself, and dropping any one of the three (either advising fact, or the rule) leaves a knowledge base that no longer entails it. The derivation and the evidence set happen to coincide here because the example is tiny; the concept that generalizes is the evidence set, together with the property that made it convincing: you cannot shrink it.

Now the definition, decoded before it is written. Let $O$ be an ontology, a finite set of axioms; in this chapter $O$ is Volume 2's academic TBox, and its size, written $\lvert O \rvert$ (the number of axioms it contains), is $14$. Let $\alpha$ be a candidate consequence, here always a subsumption between two named concepts, written $A \sqsubseteq B$ ("every $A$ is a $B$"). The symbol $\models$ is semantic entailment: $O \models \alpha$ means every interpretation that satisfies all axioms of $O$ also satisfies $\alpha$. The symbol $\subseteq$ is set inclusion, $\subsetneq$ is proper inclusion (a subset that is not the whole set), the quantifier $\forall$ reads "for all", and a slash through a symbol negates it, so $\not\models$ reads "does not entail". Then:

$$J \text{ is a justification for } O \models \alpha \quad\text{iff}\quad J \subseteq O, \qquad J \models \alpha, \qquad \text{and} \qquad \forall\, J' \subsetneq J:\; J' \not\models \alpha .$$

The three conjuncts read: $J$ uses only axioms actually in the ontology; $J$ forces the conclusion on its own; and no proper subset of $J$ still forces it. The literature also calls $J$ a MinA (minimal axiom set), and for the special case where $\alpha$ says a concept is unsatisfiable ($A \sqsubseteq \bot$, with $\bot$ the empty concept), a MUPS (minimal unsatisfiability-preserving sub-TBox); naming the object and posing the debugging problem it serves is where axiom pinpointing began [2]. Note what the definition does not mention: rules, proof trees, or any reasoner at all. A justification is a property of the ontology and the conclusion alone, which is exactly what makes it the right unit for explanation (a human can audit a small axiom set), for debugging (an unwanted conclusion's justifications localize the fault), and for the rest of this volume (a faithfulness probe needs a ground-truth "real reason" to compare against, and this is it).

One consequence of the definition needs deriving now, because three later arguments lean on it. Entailment in EL, as in every description logic of this series, is monotone: adding axioms never removes consequences. Precisely, if $J \subseteq J'$ and $J \models \alpha$, then $J' \models \alpha$. The proof is one sentence of semantics: any interpretation satisfying every axiom of $J'$ in particular satisfies every axiom of $J$ (they are all in $J'$), hence satisfies $\alpha$ because $J \models \alpha$. Monotonicity has a contrapositive we will use constantly: if the larger set fails to entail, so does every subset of it.

Monotonicity immediately buys the chapter's cheapest theorem, the drop-any-one certificate. Suppose $J \models \alpha$ and, for every axiom $i \in J$ (the symbol $\in$ reads "is a member of"), the single-deletion set $J \setminus \{i\}$ ($J$ with axiom $i$ removed) fails to entail $\alpha$. Then $J$ is minimal, over all proper subsets, not just the single-deletion ones. Why: suppose some $J' \subsetneq J$ entailed $\alpha$. Being proper, $J'$ misses at least one axiom $i \in J \setminus J'$, so $J' \subseteq J \setminus \{i\}$. Monotonicity applied to $J' \models \alpha$ then forces $J \setminus \{i\} \models \alpha$, contradicting the per-axiom check. So $\lvert J \rvert$ oracle checks certify minimality against all $2^{\lvert J \rvert}$ subsets. This is the audit the companion runs on every justification it ever returns.

One object, three uses: the justification as minimal evidence (left), the expand-contract search that finds one (center), and the hitting-set tree that finds all of them and prices the repair (right). Original diagram by the authors, created with AI assistance.

The oracle discipline: one primitive, any reasoner

Everything in this chapter is black-box axiom pinpointing: the reasoner is never opened, instrumented, or trusted to explain itself. The only primitive any algorithm below may call is an entailment oracle, one function of one shape: given an axiom subset and a candidate subsumption, does the subset entail it? The companion implements the oracle by re-running Volume 2's from-scratch EL machinery on exactly the given axioms: normalize rewrites them into the four normal forms (el_completion.py lines 69–154), complete saturates the subsumer map $S$ with the completion rules CR1–CR4, the bottom rule, and the role-chain rule (el_completion.py lines 177–261), and the answer is read off the saturated $S$. The wrapper, with its bookkeeping (justifications.py lines 100–129):

STATS = {"saturations": 0, "oracle_calls": 0}
_SAT_CACHE: dict = {}   # frozenset of axiom ids -> saturated subsumer map S


def _saturate(ids: frozenset):
    """The saturated subsumer map S of the sub-TBox {axiom ids}: Volume 2's
    normalize + complete run on exactly those axioms (memoized per subset)."""
    if ids not in _SAT_CACHE:
        normalized, _fresh = elc.normalize([AXIOMS[i - 1] for i in sorted(ids)])
        S, _R = elc.complete(normalized)
        _SAT_CACHE[ids] = S
        STATS["saturations"] += 1
    return _SAT_CACHE[ids]

def is_entailed(ids, sub: str, sup: str) -> bool:
    """The oracle every algorithm below is built on: does the axiom SUBSET
    ``ids`` (1-based ids into AXIOMS) entail ``sub ⊑ sup``?"""
    STATS["oracle_calls"] += 1
    return _entailed_by(_saturate(frozenset(ids)), sub, sup)

Two details of the wrapper are load-bearing. First, _entailed_by (justifications.py lines 115–122) adds one semantic clause beyond "is the superclass in $S(\text{sub})$": if $\bot \in S(\text{sub})$, the concept is unsatisfiable, its extension is empty in every model, and the empty set is a subset of everything, so an unsatisfiable concept is subsumed by every concept. Without that clause, pinpointing on $A \sqsubseteq \bot$ queries would silently disagree with the semantics. Second, the memoization cache _SAT_CACHE counts saturations separately from oracle calls: the algorithms below re-ask about the same subsets often, and the committed run answers 232 entailment calls with only 90 actual saturations. Each saturation is one full run of a polynomial-time procedure, so an oracle call is cheap but not free, and every algorithm in this chapter will be priced in oracle calls.

Why insist on the black box? Because it makes the entire toolkit reasoner-independent. The oracle here happens to be Volume 2's from-scratch completion engine; it could be ELK, HermiT, Konclude, or any sound-and-complete decision procedure for the logic, and not one line of the pinpointing code would change. That portability is what made black-box search the practical route to justifications for OWL DL (the description-logic profile of the Web Ontology Language), where reasoners are large, highly optimized, and not built to explain themselves [3]. The alternative is glass-box pinpointing: open the reasoner and make every inference carry a label recording which axioms it used, so that when the conclusion appears it arrives wearing a pinpointing formula, a monotone Boolean formula over axiom variables whose minimal satisfying valuations are exactly the justifications [4]. Glass-box methods pay once, during reasoning, instead of per oracle call, but they must be engineered anew inside each reasoner and can distort its optimizations. The trade will return in the scale section; here we stay black-box on purpose, because Volume 5 will spend six more parts treating systems as opaque oracles, and this chapter is the discipline in its cleanest form.

One justification: expand and contract

The first algorithm finds a single justification, and it is two loops. Expand: grow a support set, adding axioms in a fixed order, until the oracle first says it entails; that prefix is an entailing set, usually far from minimal. Contract: walk through the support one axiom at a time; tentatively delete the axiom, ask the oracle whether the entailment survives, commit the deletion if it does and roll it back if it does not. The contraction pass serves the debugging problem that axiom pinpointing's founding paper posed [2]; the deletion loop itself, packaged inside the expand-contract search (the original calls the two phases expand and shrink), is what made black-box justification extraction practical [3]. The committed loops (justifications.py lines 150–155 and 158–162; the log bookkeeping between and after them is elided):

    # -- Expand ------------------------------------------------------------
    support: list = []
    for i in sorted(ids):
        support.append(i)
        if is_entailed(support, sub, sup):
            break

    # -- Contract (deletion-based) ------------------------------------------
    just = set(support)
    for i in list(support):
        if is_entailed(just - {i}, sub, sup):
            just.discard(i)

Why does one pass suffice? The loop maintains an invariant: at every point, the working set just entails $\alpha$. It holds at entry (expand stopped at the first entailing prefix) and every committed deletion was confirmed by the oracle, so it holds at exit: the result entails. Minimality is the subtler half, because the loop tests each axiom only once, against whatever the working set happened to be at that moment, not against the final result. Monotonicity closes the gap. Write $R$ for the returned set and take any axiom $i \in R$. When the loop tested $i$, its working set $W$ satisfied $W \supseteq R$ (the superset symbol $\supseteq$ says $W$ contains every member of $R$, which holds because the set only shrinks as the loop proceeds and everything in $R$ survived to the end), and the test failed: $W \setminus \{i\} \not\models \alpha$, which is why $i$ was kept. Now $R \setminus \{i\} \subseteq W \setminus \{i\}$, and the contrapositive of monotonicity (a non-entailing set has no entailing subset) gives $R \setminus \{i\} \not\models \alpha$. That is exactly the drop-any-one condition for every $i \in R$, and the certificate theorem of the first section upgrades it to full minimality: $R$ is a justification. The companion does not merely trust this argument; it re-runs the certificate explicitly before returning, one oracle call per axiom (justifications.py lines 168–173):

    # -- The minimality audit (per axiom, against the oracle) ----------------
    assert is_entailed(result, sub, sup), "contraction destroyed the entailment"
    for i in sorted(result):
        assert not is_entailed(result - {i}, sub, sup), (
            f"not minimal: axiom ({i}) is redundant in {fmt_just(result)}")

The committed trace for the query Dean ⊑ Researcher shows every decision:

[2] ONE justification by expand-contract — query: Dean ⊑ Researcher
  expand   : support grows in axiom order; axioms 1..8 first entail the query (support size 8)
  contract : (1) dropped  (2) dropped  (3) dropped  (4) KEPT  (5) KEPT  (6) dropped  (7) dropped  (8) KEPT
  MinA     : {4, 5, 8}
  audit    : dropping any single axiom of the MinA breaks the entailment (asserted, per axiom, for every query)

Read the contraction like a story. The support is axioms 1 through 8, the first prefix that entails. Axiom 1 (Professor ⊑ Researcher) is deleted, and the entailment survives, because a second route exists: Dean ⊑ Professor, Professor ⊑ ∃advises.Student, and ∃advises.⊤ ⊑ Researcher still chain to the conclusion. Axioms 2, 3, 6, 7 fall for the plainer reason that they never mattered. Axioms 4, 5, 8 each break the entailment when removed, so each is kept, and the result is the three-axiom detour {4, 5, 8}. Notice that the algorithm's answer depends on the deletion order: had the loop tried axiom 4 before axiom 1, it would have found the two-axiom justification {1, 8} instead. Expand-contract promises a justification, never a canonical or smallest one.

The cost accounting is clean. Let $n = \lvert O \rvert$ be the ontology size. Expand makes at most $n$ oracle calls (one per prefix), contract exactly $\lvert \text{support} \rvert \le n$ calls, and the audit $1 + \lvert R \rvert$ more, so one justification costs at most $2n + \lvert R \rvert + 2$ oracle calls including the initial entailment check. That count grows linearly in $n$, written $O(n)$ in the big-O notation for growth rates (a standard, if unfortunate, clash with the letter $O$ for the ontology), and each call is a polynomial saturation. Finding one reason is genuinely cheap. Finding all of them is where the structure, and the cost, appears.

All justifications: Reiter's hitting-set tree

Why is one justification not enough? The committed run answers with the ontology itself. The entailment Professor ⊑ Researcher has two justifications: the direct axiom {1}, and the detour {4, 5} (a professor advises some student, and anything that advises anything is a researcher). This redundancy is real, not staged for the chapter: Volume 2's ontology.py notes on axiom 5 that the completion rules re-derive axiom 1 from 4 and 5. The consequence for anyone acting on a justification is immediate: delete axiom 1, and the entailment still stands, propped up by the other reason. Explanation can sometimes afford to show one reason; debugging cannot, because a repair that kills one justification and leaves another alive has repaired nothing. We need the complete set.

The classical route to all justifications is Reiter's hitting-set tree (HST), imported from model-based diagnosis [1] and adapted to ontologies [3]. Decode the idea before the formalism. We have found one justification $J$. Where could a different justification $J^{*}$ be hiding? Since $J^{*} \ne J$ and both are minimal, neither contains the other, so $J^{*}$ must miss at least one axiom of $J$. Therefore: for each axiom $i \in J$, delete $i$ from the ontology and search the remainder. Any other justification survives at least one of these deletions and will be found in that branch. Recurse, and the search space becomes a tree: each node is labeled with a justification of the ontology minus the deletions on its path; each edge deletes one axiom of its parent's label; a closed leaf is a node where the remaining axioms no longer entail, meaning the path's deletion set has hit every justification. The committed core (justifications.py lines 195–219):

    root = single_justification(ids, sub, sup)
    if root is None:
        return set(), 0
    justs: list = [root]          # discovery order (kept for determinism)
    expanded: set = set()         # hitting sets (paths) already handled
    nodes = 1
    queue: list = [(root, frozenset())]   # (node label, deletions so far)
    while queue:
        label, deleted = queue.pop(0)     # FIFO: breadth-first, deterministic
        for i in sorted(label):
            path = deleted | {i}
            if path in expanded:          # early path termination
                continue
            expanded.add(path)
            nodes += 1
            reuse = next((j for j in justs if not (j & path)), None)
            if reuse is not None:         # node-label reuse: no oracle work
                queue.append((reuse, path))
                continue
            j = single_justification(ids - path, sub, sup)
            if j is None:
                continue                  # closed leaf: path hits every MinA
            justs.append(j)
            queue.append((j, path))
    return set(justs), nodes

Now the completeness argument, in full, because it is the theorem the whole construction rests on. Let $J^{*}$ be any justification of $O \models \alpha$. Claim: some node of the tree is labeled exactly $J^{*}$. Follow a path chosen as follows. Start at the root, whose deletion set is $D = \emptyset$ (the empty set), disjoint from $J^{*}$. At any node with label $J$ and deletion set $D$ satisfying $D \cap J^{*} = \emptyset$ (the intersection symbol $\cap$ collects the common elements; disjointness means no axiom of $J^{*}$ has been deleted on this path): if $J = J^{*}$, we are done. Otherwise $J \ne J^{*}$, and minimality works both ways: $J \subsetneq J^{*}$ would contradict $J^{*}$'s minimality, and $J \supsetneq J^{*}$ would contradict $J$'s, so neither contains the other and the difference $J \setminus J^{*}$ is non-empty. Pick $i \in J \setminus J^{*}$ and follow the edge deleting $i$. The child's deletion set $D \cup \{i\}$ (the union symbol $\cup$ pools the members of both sets) is still disjoint from $J^{*}$ (we chose $i$ outside $J^{*}$), so the remaining ontology $O \setminus (D \cup \{i\})$ still contains all of $J^{*}$, entails $\alpha$ by monotonicity, and the child is therefore labeled with some justification, not closed. Repeat. Each step grows $D$ by one axiom drawn from the finite set $O \setminus J^{*}$, so after at most $\lvert O \rvert - \lvert J^{*} \rvert$ steps the walk must halt, and the only way it halts is the case $J = J^{*}$. Every justification labels a node; the tree finds them all. Termination of the whole search is the same finiteness: every path's deletion set strictly grows inside a finite ontology.

Two optimizations in the code are not cosmetic; they are the load-bearing prunes, introduced with Reiter's tree and kept in its ontology adaptation [1][3]. Early path termination: two paths that delete the same set of axioms lead to identical subproblems (only the set matters, not the order), so a deletion set already expanded is never expanded again; this is the expanded check. Node-label reuse: if some already-found justification $J$ is disjoint from the current path's deletions, then $J$ survives intact in the remaining ontology, still entails, and is still minimal there (minimality is inherited downward: a proper subset of $J$ that entailed inside the smaller ontology would entail inside $O$ too, by monotonicity, contradicting $J$'s minimality in $O$). So $J$ can label the node with zero oracle work; this is the reuse line.

The committed enumeration, with the tree sizes:

query	MinAs found	HST nodes explored	brute force agrees?
Professor ⊑ Researcher	2 : {1}, {4, 5}	4	EXACT match
Dean ⊑ Researcher	3 : {1, 8}, {5, 9}, {4, 5, 8}	13	EXACT match
TenuredStudent ⊑ ⊥	1 : {6, 10, 11}	4	EXACT match
TenuredStudentAdvisor ⊑ ⊥	1 : {6, 10, 11, 12}	5	EXACT match
Student ⊑ Professor	not entailed: none	0	—

Dean ⊑ Researcher deserves a slow read, because its three justifications overlap in instructive ways. {1, 8} is the inheritance route: a dean is a professor, a professor is a researcher. {5, 9} is the pure role route: a dean advises some professor, and advising anything makes you a researcher. {4, 5, 8} is the hybrid found by expand-contract above: a dean is a professor, a professor advises some student, advising makes a researcher. Note that {4, 5, 8} shares axiom 8 with the first justification and axiom 5 with the second, yet is minimal itself: no proper subset of it entails. Justifications form an antichain (no one contains another, immediately from minimality), but they may overlap freely, and that overlap is exactly what will make repair a hitting-set problem rather than a pick-one problem.

The final column of the table is the luxury only a toy can afford, and the companion spends it deliberately. brute_force_all (justifications.py lines 224–253) enumerates every one of the $2^{14} = 16{,}384$ subsets of the TBox, saturates each one fresh (bypassing the cache, sharing nothing with the HST run except the completion engine), marks the entailing subsets, and keeps exactly the minimal ones; minimality needs only the one-deletion children, by the same monotonicity argument as the drop-any-one certificate. The harness then asserts exact set equality, HST versus brute force, on all four entailments (justifications.py lines 328–331):

    for q in QUERIES:
        assert single[q] in hst[q], f"single MinA missing from HST on {q}"
        assert hst[q] == brute[q], f"HST != brute force on {q}"
        assert hst[q] == EXPECTED[q], f"reason set changed on {q}"

and the committed cost line makes the point of the whole construction numerically:

  oracle work for [2]+[3]: 90 saturations, 232 entailment calls (memoized); brute force: 16384 saturations

Ninety saturations against sixteen thousand: the hitting-set tree explored 26 nodes total across the four queries and provably found everything the exhaustive sweep found. At 14 axioms the exhaustive sweep is a feasible referee; at SNOMED CT's several hundred thousand axioms, $2^{\lvert O \rvert}$ is not a number, and the tree, with its prunes, is the algorithm.

Pinpointing as debugging: repairs are hitting sets

Now invert the lens. So far the entailments were wanted and the justifications were explanations. The academic TBox also contains a bug, planted in Volume 2 and finally diagnosed here: TenuredStudent is unsatisfiable, that is, the TBox entails TenuredStudent ⊑ ⊥, so no individual can ever be a tenured student without contradiction. The justification of an unwanted entailment is not an explanation but an indictment: it names, exactly and minimally, the axioms among which the fault lies. The committed diagnosis:

[5] pinpointing as debugging — why is TenuredStudent unsatisfiable?
  the single MinA {6, 10, 11} (Schlobach & Cornet's MUPS of the concept):
    ( 6) Professor ⊓ Student ⊑ ⊥
    (10) TenuredStudent ⊑ Professor
    (11) TenuredStudent ⊑ Student
  minimal repairs = minimal hitting sets of all MinAs (Reiter's diagnoses):
    remove ( 6) → TenuredStudent satisfiable again (verified against the oracle)
    remove (10) → TenuredStudent satisfiable again (verified against the oracle)
    remove (11) → TenuredStudent satisfiable again (verified against the oracle)

The story is three axioms long: tenured students are professors, tenured students are students, and professors and students are disjoint. Note what pinpointing did not do: it did not say which axiom is wrong. That is a modeling judgment (probably the disjointness axiom 6 is too strong), and no algorithm can make it. What the algorithm can do is delimit the choice: a repair is a set of axioms $R \subseteq O$ whose removal kills the entailment, $O \setminus R \not\models \alpha$, and the justifications determine the repairs completely.

Theorem (repair duality). $R$ is a repair for $\alpha$ if and only if $R$ is a hitting set of the family of all justifications, meaning $R \cap J \ne \emptyset$ for every justification $J$: the repair removes at least one axiom from each.

Both directions are short, and both are monotonicity again. Suppose $R$ misses some justification $J$ entirely, $R \cap J = \emptyset$. Then every axiom of $J$ survives the removal, $J \subseteq O \setminus R$, and monotonicity applied to $J \models \alpha$ gives $O \setminus R \models \alpha$: not a repair. Conversely, suppose $R$ hits every justification, and imagine the removal failed, $O \setminus R \models \alpha$. Any finite entailing set contains a minimal entailing subset: run the contraction loop on it, deleting axioms while entailment survives; the loop terminates because the set is finite and strictly shrinks, and it stops precisely at a set passing the drop-any-one test, a justification. So $O \setminus R$ would contain a justification $J \subseteq O \setminus R$, which is a justification of $O$ too, and $R \cap J = \emptyset$, contradicting the hypothesis. Hence the minimal repairs are exactly the minimal hitting sets, which is Reiter's original duality with the vocabulary swapped: axioms for components, justifications for minimal conflict sets, repairs for diagnoses [1]. Ontology debugging is a special case of diagnosis from first principles, which is why the debugging chapter of this volume opened with a 1987 citation.

The companion computes the minimal hitting sets by smallest-first enumeration over the union of the justifications, discarding any candidate that contains an already-found hitting set (justifications.py lines 258–272), and then closes the loop the only honest way, by handing each claimed repair back to the oracle (justifications.py lines 340–343):

    assert unsat_repairs == {frozenset({6}), frozenset({10}), frozenset({11})}
    for rep in sorted(unsat_repairs, key=sorted):
        assert not is_entailed(ALL - rep, "TenuredStudent", BOT), (
            f"repair {fmt_just(rep)} did not restore satisfiability")

Here the family has a single member, so the minimal hitting sets are the three singletons and each one-axiom removal verifiably restores satisfiability. With overlapping families the problem earns its complexity. Precisely: given the family of justifications and an integer $k$ (a size budget), deciding whether a hitting set of size at most $k$ exists is NP-complete, because it is the classical minimum hitting set problem, equivalent to set cover (NP is nondeterministic polynomial time, the class of decision problems whose yes-answers can be checked in polynomial time; NP-complete problems are the hardest of them, and NP-hard means at least that hard). Finding a minimum-cardinality repair is therefore NP-hard. Reiter's paper sidesteps the hardness rather than analyzing it: because his tree grows breadth-first, diagnoses arrive in order of increasing size, so a search that wants only the small repairs can simply stop at a size budget [1]. The proof of the hardness is beyond this volume; what the companion demonstrates instead is the duality the hardness lives on, exact and oracle-verified at toy scale. And a second, quieter caution from the committed run: the concept TenuredStudentAdvisor is also unsatisfiable, with MinA {6, 10, 11, 12}, because axiom 12 forces it to advise some TenuredStudent and the bottom rule propagates the contradiction back along the role. Repairing TenuredStudent by removing any of 6, 10, 11 happens to hit this second MinA too and heals both concepts at once; in general, though, deleting whole axioms is a blunt instrument, since an axiom may carry several claims of which only one is faulty. Refining justifications below the axiom level, so that a repair can weaken axiom 6 rather than delete it, is the subject of laconic justifications [5], and it returns in the unsolved part.

Scale, honestly

Everything above is exact, and the ceiling is stated in the same breath. First, the population being enumerated can be enormous: there are families of TBoxes, even in EL, whose size grows only linearly in a parameter $n$ while a single entailment has $2^{n}$ justifications, so the output of all-justifications enumeration is exponential before any algorithmic cleverness is spent; the construction is worked out in the paper that brought pinpointing to the EL family, which also proves that even asking whether a justification within a given size bound exists is NP-complete [6]. The proofs are beyond this volume; the companion demonstrates the opposite luxury instead, a 14-axiom world where the complete enumeration is small (seven MinAs across four entailments) and independently checkable. The field's three levers against the ceiling, one paragraph each:

Shrink the haystack: modules. A justification for $A \sqsubseteq B$ can only use axioms that are, in a precise syntactic sense, reachable from the signature of the entailment; the black-box line exploited this from the start by expanding the support along selection functions rather than taking the whole ontology [3]. The mature form of the idea is locality-based module extraction: a cheap syntactic pass extracts a subset of the ontology provably guaranteed to contain every justification of the target entailment, and all pinpointing then runs inside the module [7]. On SNOMED-scale inputs this is routinely the difference between minutes and never.

Open the reasoner: the pinpointing formula. Glass-box pinpointing labels every derived consequence with a monotone Boolean formula over axiom variables recording how it was derived; the label of the goal is the pinpointing formula, whose minimal satisfying valuations are exactly the justifications, computed in one instrumented run instead of hundreds of oracle calls [4]. The costs are real: the instrumentation must be re-engineered per calculus, it can break the reasoner's optimizations, and the formula itself can blow up. The theory delimits precisely when it stays tractable.

Follow the proof. A consequence-based reasoner derives each subsumption by explicit rule applications, so the inference steps behind every conclusion already exist inside the run; ELK, the EL family's flagship reasoner, is built exactly this way [8], its tooling exposes those steps as proof traces, and proof-driven enumeration mines the justifications from the recorded inferences by resolution rather than probing subsets blindly [9]. This is the practical middle road for EL-family ontologies: black-box generality is surrendered, but the reasoner was going to compute the proofs anyway.

Carry one sentence forward from this chapter, because the rest of the volume leans on it. A justification is ground truth for "why": the next chapter's faithfulness probes ask whether a system's self-reported explanation matches the evidence that actually forces the answer, and Part VII scores SATORI's attention traces against exactly this standard. Everything downstream that audits a reason presupposes that reasons of this checkable kind exist.

The unsolved part

Three honest gaps. First, scale: enumeration at the size of SNOMED CT remains expensive in the worst case for a reason no engineering removes, since the answer itself can be exponentially long; modules, glass-box tracing, and proof mining move the constant, not the ceiling. Second, selection: when an entailment has dozens of justifications, which one should a human see first? The empirical literature on what actually helps ontology engineers, and lay users, understand and fix an entailment is thin, decades younger than the algorithms. Third, granularity: whole axioms are often the wrong unit, since one axiom can bundle several claims, and laconic justifications, which keep only the logically active parts of each axiom, trade canonical form for readability in ways that are still being negotiated [5]. The object is settled; its human interface is not.

Why it matters

This chapter is the volume's foundation stone because it produces the one thing every later trust instrument needs: a checkable reason with a mathematical definition, an algorithm, and a certificate. The series has been building toward this division of labor since Volume 1: symbolic systems are not merely accurate, they are auditable, and the justification is what auditable means, made formal. For the reader's own research the transferable assets are the two disciplines. The oracle discipline (treat the system as a black box, define the one primitive, price everything in calls to it) applies verbatim when the oracle is a neural model rather than an EL reasoner, and Volume 5 will apply it that way repeatedly. The certificate discipline (never return a minimal object without its drop-any-one audit; never trust an enumeration you have not, at least once at toy scale, checked against brute force) is what separates a demonstration from an anecdote, and the committed asserts of justifications.py are its working example.

Key terms

• Justification (MinA, minimal axiom set): a subset $J \subseteq O$ with $J \models \alpha$ such that no proper subset of $J$ entails $\alpha$; the minimal evidence for an entailment.
• MUPS (minimal unsatisfiability-preserving sub-TBox): a justification for a concept-unsatisfiability entailment $A \sqsubseteq \bot$.
• Monotonicity: in EL and its relatives, adding axioms never removes consequences; if $J \subseteq J'$ and $J \models \alpha$ then $J' \models \alpha$. The lemma behind the drop-any-one certificate, the contraction proof, and the repair duality.
• Drop-any-one certificate: the $\lvert J \rvert$ oracle checks (each single deletion breaks the entailment) that, by monotonicity, certify minimality against all $2^{\lvert J \rvert}$ subsets.
• Expand-contract: grow a support until it first entails, then delete axioms one at a time, keeping each deletion the entailment survives; returns one justification in $O(\lvert O \rvert)$ oracle calls.
• Black-box vs glass-box pinpointing: black-box uses only an entailment oracle and works with any reasoner; glass-box instruments the reasoner to emit a pinpointing formula, a monotone Boolean formula whose minimal satisfying valuations are the justifications.
• Hitting-set tree (HST): the enumeration tree whose nodes are justifications of the ontology minus the path's deletions and whose edges delete one axiom of the parent's label; complete for all justifications.
• Repair / diagnosis duality: $R$ removes the entailment iff $R$ hits every justification; minimal repairs are the minimal hitting sets, Reiter's diagnoses under a change of vocabulary.
• Laconic justification: a justification refined below the axiom level, keeping only the logically active parts of each axiom.

Where this leads

This chapter's explanations were extracted from a system that cannot lie about its reasons: the oracle's answer is determined by the axioms, and the justification is checkable evidence. The next systems Volume 5 audits are not like that. A neural model, asked why, produces a story, and nothing in its architecture guarantees the story matches the computation. Faithfulness builds the probes that catch the mismatch, and the justification defined here is the gold standard those probes are calibrated against: an explanation is faithful exactly when it plays the role for the model that a MinA plays for the oracle.

---

Companion code: examples/frontier/justifications.py implements the entailment oracle over Volume 2's examples/symbolic/el_completion.py, expand-contract with its per-axiom minimality audit, Reiter's hitting-set tree with both prunes, the brute-force referee over all 16,384 axiom subsets, and the verified repairs of the TenuredStudent contradiction. Run python3 examples/frontier/justifications.py to reproduce every number in this chapter; the run is deterministic and every claim is guarded by an assert.