Chapter 6 – Introduction to Truth Maintenance Systems

Your first system that remembers why it believes things, and revises belief automatically when the reasons change. companion index

The big idea

So far in the book the rule engines (TRE in chapters 4-5) treat belief as a simple yes/no question: a fact is believed if and only if it is sitting in the database. That is fine while you are only ever adding facts. The trouble starts the moment you want to change your mind. Suppose you assumed it was raining, derived a dozen downstream conclusions from that, and now you learn it is not raining after all. Which of those dozen conclusions should you keep? The ones that also follow from other facts, and only those. A plain database has no idea, because it never recorded why anything was added.

A Truth Maintenance System (TMS) fixes this by separating two jobs that the rule engine had previously smeared together:

Inference – figuring out what follows from what. This stays with the rule engine.
Belief – deciding, at any given moment, which conclusions are currently justified. This moves into the TMS.

The rule engine hands the TMS little records of the form “these antecedents justify this consequence,” and from then on the TMS keeps every node’s belief label correct as assumptions come and go, incrementally, without re-running any rules. The payoff is three things you get almost for free once you adopt this discipline:

Caching. A conclusion already derived is just a label lookup, never a recomputation.
Explanation. Because every belief points at its supporting record, the system can answer “why do you believe this?” by walking the support chain back to its roots.
Automatic belief revision. Retract an input and everything that depended on it (and nothing else) loses belief, automatically.

This chapter introduces the simplest TMS, the justification-based TMS (JTMS). It is deliberately the small one: it can only ever say a node is IN (believed) or OUT (not currently believed). It can never represent “this is false.” That limitation is exactly what later chapters lift when they move to the logic-based TMS (LTMS), so understanding precisely what the JTMS can and cannot do is the whole point of starting here.

The repository’s implementation of everything in this chapter lives in ../src/ltms/jtms.py (the engine) and ../src/ltms/jtre.py (a thin rule-engine wrapper around it).

Concepts, step by step

Nodes and the IN/OUT label

The atoms of a JTMS are nodes. Each node stands for one proposition – “it is raining,” “the lamp lights,” “x = 6.” Every node carries a single belief label:

IN – the node is currently believed, because it has at least one currently valid reason.
OUT – the node is not currently believed.

The single most important warning in the whole chapter: OUT does not mean false. It means “I have no current reason to believe this.” A JTMS literally cannot represent falsity; it has no machinery for negation. “We do not currently believe it is raining” and “we believe it is not raining” are different statements, and the JTMS can only express the first. (Distinguishing the two is the entire reason the LTMS exists, two chapters from now.)

In the code, the label is an enum and the node is a small object (../src/ltms/jtms.py):

class Belief(Enum):
    IN = "IN"
    OUT = "OUT"

A Node records its label, its current support (more on this below), the list of justs (justifications that could make it IN), and the list of consequences (justifications in which it appears as an antecedent, so the engine knows who to revisit when this node’s belief changes).

Justifications: the Horn-clause unit of inference

A justification is a record of one inference step:

antecedents  =>  consequence

Logically this is a definite clause (a Horn clause): “if all of the antecedent nodes are believed, then the consequence node is believed.” A justification also carries an informant – a tag naming who or what created it (a rule name, a procedure name like multiply). The informant is what lets explanations say how a conclusion was reached, not just that it was.

class Justification:
    # antecedents => consequence, tagged with an informant
    index; informant; consequence; antecedents

Two special shapes of justification are worth naming:

A justification with no antecedents is a premise: an unconditionally believed fact. (assert_ in the engine installs exactly this.)
A node may instead be marked an assumption and enabled. An enabled assumption is believed not because of a justification but because you chose to entertain it. Crucially, assumptions can be retracted; premises cannot. The code marks an enabled assumption with a special sentinel value, ENABLED_ASSUMPTION.

So a node’s support is overloaded three ways, and reading it tells you exactly why the node is IN:

`support` value	meaning
`None`	the node is `OUT`
a `Justification`	derived (empty antecedents => it is a premise)
`ENABLED_ASSUMPTION`	believed because it is an enabled assumption

Well-founded support (the anti-circularity rule)

Here is the subtle invariant that makes a TMS correct rather than merely plausible: belief must be well-founded. Every IN node’s support must ultimately bottom out in premises and enabled assumptions, following a finite, non-circular chain. The forbidden situation is two nodes propping each other up with nothing underneath: “B is IN because C is IN; C is IN because B is IN.” That is internally consistent but grounded in nothing, and a naive implementation can drift into it. Avoiding it is the reason retraction is done in two carefully ordered phases, described below.

Adding belief: the monotone forward sweep

Anything that can only add belief is easy and is handled by a forward sweep that only ever flips nodes OUT -> IN:

Install the new justification (or enable an assumption).
Check whether it is now satisfied – its consequence is currently OUT and all of its antecedents are IN.
If so, mark the consequence IN, make this justification its support, and propagate: revisit every justification that has the newly-IN node as an antecedent, repeating the check.

In the code this is _propagate_inness, gated by _check_justification (consequence OUT and all antecedents IN). It is a plain work-list closure, and because it only adds belief it can never loop or contradict itself:

def _check_justification(self, just):
    return just.consequence.is_out and self._justification_satisfied(just)

@staticmethod
def _justification_satisfied(just):
    return all(a.is_in for a in just.antecedents)

Removing belief: the two-phase retraction

Retraction is the hard case, and the place a sloppy TMS goes wrong. When you retract an enabled assumption, some conclusions lose their only support and must go OUT, but others that seemed to depend on it may actually have an alternative reason and should stay IN. You cannot decide both at once. The JTMS splits the work into two strictly ordered phases:

Phase 1 – propagate outness. Walk forward from the retracted node and label OUT every node whose current support flows through it. The test is by identity: a node is knocked out only if its support is this exact justification (the one whose antecedent just disappeared). This produces a set of “forgotten” nodes – everything that was leaning, right now, on the retracted node.

def _propagate_outness(self, node):
    out = []
    queue = list(node.consequences)
    while queue:
        j = queue.pop(0)
        conseq = j.consequence
        if conseq.support is j:          # identity: this just IS its support
            self._make_node_out(conseq)
            out.append(conseq)
            queue.extend(conseq.consequences)
    return out

Phase 2 – find alternative support. Only after phase 1 is complete, look at each forgotten node and ask: does it have some other satisfied justification? If so, re-derive it (and re-propagate that re-found belief). A node with two independent reasons survives losing one of them; this is the phase that lets it.

def _find_alternative_support(self, nodes):
    for node in nodes:
        if not node.is_in:
            for just in node.justs:
                if self._check_justification(just):
                    self._install_support(just.consequence, just)
                    break

Why two phases and not one interleaved pass? Because interleaving readmits the ill-founded circular support described above. If you tried to re-justify B while C had not yet been knocked OUT, B could be “re-derived” from a C that is itself about to vanish, and the two would keep each other artificially alive. Clearing everything first, then re-deriving from a clean slate, is what guarantees well-foundedness. This two-phase structure is reused almost verbatim by the LTMS later, so it is worth getting clear here.

Contradictions: signal, do not solve

A node can be marked contradictory. The JTMS’s job regarding contradictions is modest: it merely signals when a contradictory node becomes IN, by calling a handler (the default one raises JTMSContradiction). It does not try to fix the contradiction. Resolving it – figuring out which assumption to retract to make the trouble go away – is dependency-directed backtracking, and that is the caller’s responsibility. The hook the caller needs is assumptions_of_node, which returns the enabled assumptions underlying a node’s current support:

def assumptions_of_node(self, node):
    # walk current well-founded support back to its enabled assumptions
    ...

Note the careful wording: it returns the assumptions of one well-founded support, not all possible supports and not a guaranteed-minimal set. That is enough to drive backtracking, and keeping it simple is deliberate.

Explanation

Because support points backward, explanation falls out for free. why_node reports whether a node is OUT, IN via an enabled assumption, or IN via a justification, naming the informant and antecedents in the latter case:

def why_node(self, node):
    if node.is_out:                       return "... is OUT."
    if node.support is ENABLED_ASSUMPTION: return "... is IN via enabled assumption."
    # else: "... is IN via <informant> <= <antecedents>"

This is the seed of the much richer proof-DAG explanations the later chapters build.

JTre: putting a rule engine on top

A bare JTMS knows about nodes and justifications but nothing about facts or rules. ../src/ltms/jtre.py (the JTRE) bridges that gap: each ground fact (a Datum, e.g. ("raining",)) owns exactly one JTMS node, and the engine offers a fact-level API:

assert_(fact) – install fact as a premise.
assume(fact, informant) – install fact as a retractable assumption.
retract(fact, informant) – withdraw an assumption (must match the informant).
justify(informant, consequent, antecedents) – record an inference between facts.
is_in(fact) / why(fact) – query belief and explanation.

It also supports belief-conditioned rules: a rule can fire when a fact merely exists (INTERN), when it becomes believed (IN), or when it becomes disbelieved (OUT). A rule that matches before the node has the required label is parked on the node and woken later by the JTMS through an injected enqueue hook. That hook is the one place the two layers touch, and the discipline is that it only queues rules – it never calls back into the TMS mid-propagation, when the database may be transiently inconsistent.

The examples, explained

The chapter’s running illustration is the classic one: a lamp that lights only while both its battery and its bulb are good. This repo captures it as a tiny world-model file, ../exercises/ch06/kb/lamp.kb:

battery ok & bulb ok -> lamp lights
assume battery ok
assume bulb ok
expect lamp lights true
retract bulb ok
expect lamp lights unknown

Read top to bottom, this is the JTMS story in six lines:

The implication is a justification: battery ok and bulb ok together justify lamp lights. 2-3. We assume both inputs – they are retractable, not premises.
With both assumptions enabled, the justification is satisfied, so lamp lights is IN. The expect ... true line self-checks this.
We retract bulb ok. Its assumption is disabled; phase 1 of retraction knocks lamp lights OUT because its only support flowed through bulb ok; phase 2 finds no alternative support.
So lamp lights is now unknown (the engine’s word for OUT). It is not false – we simply have no current reason to believe it. The second expect line confirms it.

This single example exercises the entire chapter: justification, assumption, satisfied-clause propagation IN, and two-phase retraction back OUT.

The exercise solutions add two more sharply chosen illustrations.

Multiplication as inference (Exercise 1). Treat 6 * 7 = 42 as an inference: two input nodes (x = 6, y = 7) justify a product node (z = 42) via a single multiply justification. This is a vivid demonstration that “inference” need not mean logic – any computation can be recorded as a justification, and the moment you do, you inherit caching, dependency tracking (assumptions_of_node(z) answers “which inputs does this product depend on?”), and automatic invalidation (retract x, and z falls OUT with no manual cache-busting). The example is in ../exercises/ch06/solutions.py as ex1_multiplication_as_inference.

The smallest possible TMS (Exercise 2). A roughly 30-line MiniTMS that accepts only justifications – no premises, no assumptions, no contradictions, no retraction – so belief grows monotonically and never shrinks. It exists to make the JTMS’s extra machinery visible by its absence: the full JTMS/JTRE is a strict superset that adds assumptions, two-phase retraction, and contradiction signalling on top of this monotone core. Seeing both side by side is the clearest way to understand which capability each piece buys you.

Exercises walk-through

The full paraphrased statements and answers are in ../exercises/ch06/README.md; both exercises are marked [demonstrated in code] and run by ../exercises/ch06/solutions.py.

Exercise 1 (*) – multiplication as TMS inference

The exercise asks you to (a) explain how a TMS records a multiplication, (b) give a task where caching multiplications through a TMS yields about a 10^10 speedup, and (c) judge whether treating multiplication as inference is a good idea in general.

Recording it. The two factors become input nodes, the product becomes a consequence node, and the act of multiplying is one justification with multiply as informant. Now the product is IN (cached), its dependencies are queryable, and retracting a factor relabels it OUT automatically.
The 10^10 win. The speedup appears only under an extreme demand-to-change ratio: the same product is demanded astronomically often while its inputs are held fixed. Picture an iterative solver that, on each of ~10^10 evaluations of a large expression graph, needs the same sub-product x*y, with x and y rarely flipping. Naively that is ~10^10 multiplies; through the TMS it is one multiply plus 10^10 label lookups. Spreadsheet recalc and memoized dynamic programming exhibit the same shape.
Is it worth it in general? No. A hardware multiply costs a few nanoseconds; interning nodes, allocating a justification, running propagation, and storing dependencies cost orders of magnitude more per operation. For the overwhelming majority of multiplications – computed once, never revisited, or with inputs that change as often as they are read – the bookkeeping is pure overhead. Treating computation as inference pays off only when you genuinely need dependency-driven invalidation; if you do not, plain memoization is cheaper, and if results never repeat, even memoization loses.

The runnable demo builds the justification, reads back the dependencies, watches the product fall OUT on retracting x, then come back IN on re-enabling it.

Exercise 2 (**) – a justification-only TMS

Implement the most minimal TMS possible: it accepts only justifications – no premises, no contradictions, no assumptions – and say when such a stripped-down TMS is useful.

What it is. Each node holds one bit (IN/OUT). A node is IN iff some justification has all antecedents IN. Adding a justification runs a monotone forward closure that can only flip OUT -> IN. There is no retraction and no backtracking, so belief only ever grows. You seed belief by directly marking base nodes IN (seed), then justify to add clauses.
When is it useful? Whenever belief is monotone – facts are only ever added, never withdrawn – so you never need retraction, assumptions, or backtracking. In that regime the only services you want are caching (don’t recompute a conclusion) and explanation/provenance (record why each conclusion holds). Good fits: an assert-only forward-chaining production system or deductive database used to answer “how was this derived?”; incremental, append-only materialized views that need provenance; and the teaching case – it is the smallest core the JTMS and then the LTMS are built on top of, so it is the right thing to implement first.
When does it break down? The moment you need to change your mind – retract an input, weigh mutually exclusive assumptions, or detect and recover from a contradiction – the justification-only TMS is insufficient and you need at least the full JTMS (assumptions + two-phase retraction + contradiction signalling), which is what this package provides.

The solution implements MiniTMS faithfully (about 30 lines), then runs the same conclusion through the package’s full JTMS and JTre, and finally shows the capability the minimal version simply cannot offer: giving a goal two independent justifications, retracting one, and watching belief survive (the goal is re-derived via the other route) before retracting the second and watching it finally fall OUT. That last sequence is precisely the line MiniTMS cannot do, because it has no retraction.

Try it in this repo

All commands are run from the repository root, with the virtual environment active. (Verified working as written.)

Set up once:

python -m venv .venv && . .venv/bin/activate
pip install -e ".[dev]"

Run the two worked exercises and print their labeled results:

python exercises/ch06/solutions.py

You will see, among other things, product_in_after_retracting_x: False and product_in_after_reenabling_x: True (Exercise 1’s automatic invalidation), and for Exercise 2 jtre_goal_in_after_retract_p: True followed by jtre_goal_in_after_retract_both: False (belief surviving one retraction, then failing when both supports are gone).

Run the lamp world-model file through the generic .kb runner:

python examples/run_kb.py exercises/ch06/kb/lamp.kb

Expected output:

Loaded exercises/ch06/kb/lamp.kb
  lamp lights: true
  lamp lights: unknown

The first lamp lights line is the state with both assumptions enabled; the second is after retract bulb ok. The expect lines in the file self-check, so if the engine’s behaviour ever drifted from the chapter, loading the file would fail.

Poke at the JTMS directly from a Python prompt:

from ltms import JTMS

j = JTMS("demo")
battery = j.create_node("battery ok", assumption=True)
bulb    = j.create_node("bulb ok",    assumption=True)
lamp    = j.create_node("lamp lights")

j.enable_assumption(battery)
j.enable_assumption(bulb)
j.justify_node("series-circuit", lamp, [battery, bulb])

print(lamp.is_in)          # True
print(j.why_node(lamp))    # IN via series-circuit <= battery ok, bulb ok
j.retract_assumption(bulb)
print(lamp.is_in)          # False  (OUT, not "false")
print(j.assumptions_of_node(lamp))  # []  (no current support)

Or use the fact-level JTre wrapper, which is closer to how the later chapters talk to the engine:

from ltms import JTre

e = JTre("demo")
e.assume(("battery", "ok"))
e.assume(("bulb", "ok"))
e.justify("series-circuit", ("lamp", "lights"), [("battery", "ok"), ("bulb", "ok")])
print(e.is_in(("lamp", "lights")))   # True
e.retract(("bulb", "ok"))
print(e.is_in(("lamp", "lights")))   # False

Takeaways

A TMS separates inference (what follows) from belief (what is currently justified), and moves belief-tracking into its own incremental engine.
Recording inferences as justifications (Horn clauses with an informant) buys you caching, explanation, and automatic belief revision at once.
The JTMS is the simplest TMS: a two-valued IN/OUT label per node. OUT means “no current reason,” not “false” – the JTMS cannot represent negation at all, which is exactly the gap the LTMS fills later.
Adding belief is an easy monotone forward sweep. Removing belief is the hard part and must be two-phase: knock everything OUT first, then look for alternative support, so that belief stays well-founded (no circular self-support).
The JTMS only signals contradictions; resolving them (dependency-directed backtracking, built on assumptions_of_node) is the caller’s job.
A justification-only TMS suffices for monotone, append-only reasoning where you want caching and provenance but never need to change your mind; the full JTMS adds assumptions, retraction, and contradiction handling on top.
Everything here – the support tri-value, the two-phase retraction, the signal-don’t-solve contradiction protocol – is reused by the LTMS in the following chapters, so this small system is the foundation, not a detour.

Next up: the rule engine and TMS working together in earnest, and then the move from IN/OUT to genuine three-valued logic with negation. See the companion index for the full chapter list.