A truth maintenance system

TL;DR — In 1979 Jon Doyle proposed splitting a reasoner into two parts: a problem solver that produces beliefs, and a bookkeeper that records why each belief is held and, on contradiction, retracts exactly the minimal support. It went dormant because nothing in 1980s AI accumulated enough beliefs to need it. LLM agents do: they build up long-context "memories" full of claims that contradict each other, and today they resolve contradictions by silent overwriting or not at all. Doyle's machinery — justification graphs, IN/OUT labels, dependency-directed retraction — is an almost untried, concrete attack on hallucination persistence in agent memory. And one branch of it was already spectacularly vindicated: modern SAT solvers.

The idea as Doyle had it

Doyle, then a student in Gerald Sussman's group at MIT, made a move that sounds bureaucratic and is actually deep: beliefs are not facts, they are conclusions of arguments, and the system should store the arguments.

A Truth Maintenance System (TMS — Doyle later preferred "reason maintenance," which is more honest) sits below a problem solver. The problem solver derives things; every time it asserts a belief, it must hand the TMS a justification: the set of other beliefs the new one depends on. The TMS's job is to keep the whole belief set coherent as things change.

The core data structure is a node per potential belief, each with a status of IN (currently believed) or OUT (not currently believed — which is not the same as believed false). The clever part is the justification format. A support-list justification has two parts:

• an in-list: nodes that must be IN for this justification to be valid, and
• an out-list: nodes that must be OUT.

The out-list is the payload. "Believe the meeting is at 3pm unless you believe otherwise" becomes a justification with an empty in-list and "meeting is not at 3pm" on the out-list. This gives you defaults, assumptions, and non-monotonic reasoning as first-class citizens, years before default logic and circumscription were formalized. A node is IN iff it has at least one valid justification with well-founded support — no circular chains of belief propping each other up.

When the problem solver derives a contradiction, it asserts a contradiction node, and the TMS runs dependency-directed backtracking: trace the contradiction's support back to the assumptions underlying it (nodes IN by virtue of something being OUT), pick one to retract, and — crucially — record the culprit set as a nogood so the same dead end is never explored again. Retraction is minimal and surgical: flipping one assumption relabels exactly the nodes downstream of it, and everything else stands. Compare chronological backtracking, which throws away all work since the bad choice, including work that had nothing to do with it.

The context matters: this grew directly out of Stallman and Sussman's 1977 work on the EL circuit-analysis program, where dependency-directed backtracking gave large search-space wins. Doyle abstracted the bookkeeping into a domain-independent module — arguably the first clean separation between "inference" and "belief state management" in AI.

Why it could not work then

Two limits, one computational and one — the fatal one — ecological.

Computational. A TMS runs on a machine like the PDP-10/KL-10: roughly 1 MIPS and roughly 1 MB of usable memory. Label propagation after a retraction can touch large fractions of the graph, and the non-monotonic out-lists make labeling genuinely hard (finding a well-founded labeling is NP-hard in general; de Kleer's later ATMS, which tracks all consistent assumption environments at once, has label sets exponential in the number of assumptions). Practitioners in the 1980s reported TMS overhead dominating problem-solver time on nontrivial KBs. It was real, but engineering could have chipped at it.

Ecological. The killer was that nothing needed truth maintenance. A TMS is only worth its overhead when a system (a) accumulates thousands of interdependent beliefs, (b) revises them frequently, and (c) contradicts itself in ways that matter. Expert systems of the era had hand-curated rule bases of hundreds to low thousands of rules, hand-debugged for consistency. Beliefs came from careful knowledge engineers, not from a firehose. Doyle built a transmission for a car with no engine. The TMS literature stayed lively through the late 1980s (Doyle, de Kleer, Forbus, McAllester, Reiter–de Kleer), then mostly faded with symbolic AI itself.

What changed

Three things.

The engine arrived. An LLM agent running for hours generates exactly the belief dynamics Doyle designed for: it asserts claims from retrieval, tool calls, and its own inference; those claims depend on each other; sources get updated; the model hallucinates; and downstream conclusions built on retracted premises persist, because nothing tracks dependency. "Hallucination persistence" — a wrong claim entering memory and contaminating later reasoning — is precisely an ungrounded node that should have gone OUT when its support did. Current agent memories (append-only logs, vector stores, scratchpads) handle contradiction by recency-weighted overwriting or by never noticing.

Compute stopped being the issue. Dependency graphs with 10^5–10^6 nodes and incremental relabeling are trivial on modern hardware; this is smaller than the provenance graphs databases maintain routinely.

The core algorithm was already vindicated elsewhere. Dependency-directed backtracking with nogood recording is, in direct intellectual lineage, conflict-driven clause learning — the algorithm inside every modern SAT solver (GRASP 1996, Chaff 2001, onward). CDCL solvers handle industrial instances with millions of variables, and they win precisely because of Doyle-style conflict analysis: trace the conflict to its culprit assignments, learn a clause (a nogood), backjump non-chronologically. If you want proof the idea scales, it's running inside every chip-verification pipeline on Earth.

A 2026 revival

The design almost writes itself, because Doyle's architecture is the modern agent stack with one module added. The LLM is the problem solver. The TMS is a typed graph alongside the vector store.

Keep from the paper:

• The strict separation: the LLM proposes beliefs and justifications; a deterministic, auditable module owns belief status. Never let the model relabel by vibes.
• The justification schema. Every memory write carries provenance: (claim, in-list = supporting claims/observations/tool outputs, out-list = defeaters). Out-lists map beautifully onto retrieval-augmented defaults: "believe the doc's answer unless a fresher source is IN."
• Minimal retraction with nogood recording. When a contradiction is confirmed, retract the weakest culprit assumption, propagate OUT labels downstream, and store the culprit set so the agent doesn't re-derive the same bad chain — a learned clause for the memory.

Replace:

• Discrete propositions → canonicalized natural-language claims. This is the genuinely hard new part: two sentences can contradict without being negations of each other. You'd use an NLI/entailment model (or LLM-as-judge) as a contradiction detector over claim pairs sharing entities, then have the LLM adjudicate before asserting a contradiction node. Doyle got contradiction detection for free from the problem solver; we have to pay for it, but it's a well-studied subproblem now.
• Binary IN/OUT → graded support, at least at the edges: source-reliability priors deciding which culprit to retract (retract the model's unsupported inference before the tool output; retract the older source before the newer one). Doyle's labels can stay binary; the culprit-choice heuristic becomes learned. (Probabilistic soft-TMS hybrids exist in the literature but were never resolved cleanly — this is open.)
• Exhaustive justification recording → selective recording. Not every token deserves a node; the write policy (what becomes a tracked belief) is itself a learnable component.

The experiment: long-horizon benchmarks where ground truth changes mid-episode or where an early hallucination should poison later answers — multi-session QA with fact updates, long software-maintenance tasks, research agents over evolving sources. Measure contamination: how often a retracted or superseded premise still influences later outputs, TMS-memory versus vector-store baseline. My prediction is a large win on contamination and auditability at modest latency cost, with the interpretability side effect nearly free: every answer comes with a machine-checkable derivation tree, which is the audit trail everyone claims to want.

Already tried? Descendants? Open questions

Partially. CDCL is the triumphant descendant in search. Belief revision became a theory field (AGM postulates, 1985) with little systems contact. Data provenance and incremental view maintenance in databases are TMS ideas wearing different clothes. On the LLM side, there is scattered recent work — knowledge-graph agent memories, self-consistency checking, memory-editing methods like ROME/MEMIT (which edit weights, not memory, and famously lack minimality) — but to my knowledge no published system implements the full loop: justification-carrying memory writes, contradiction nodes, minimal retraction with propagation, and nogoods. The combination is close to untried, which is unusual for an idea this well-specified.

Open: claim canonicalization at scale; whether LLMs can emit faithful in-lists for their own inferences (they confabulate rationales — the justification extractor may need to be a separate verified step); graded belief in the labeling itself; and whether nogood memories transfer across episodes into something like learned epistemic habits.

Where to read it

The paper is A Truth Maintenance System, Artificial Intelligence 12(3), 1979 (doi:10.1016/0004-3702(79)90008-0) — bibliographic details verified. It's long but readable; the IN/OUT-list mechanism is worth absorbing directly. Read alongside: Stallman & Sussman (1977) on dependency-directed backtracking, de Kleer's An Assumption-based TMS (1986) for the parallel-worlds variant, Forbus & de Kleer's Building Problem Solvers (1993) for working code, and Marques-Silva & Sakallah's GRASP paper (1996) to watch Doyle's backtracker conquer SAT. Then look at any current LLM agent-memory paper and notice what's missing.