Chapter 7 – Justification-Based Truth Maintenance Systems (JTMS)

A friendly tour of the simplest truth maintenance system: how it tracks why you believe something, and how it cleanly takes beliefs back. Back to the companion index.

The big idea

Suppose you are reasoning forward from some facts and rules. You conclude “the ground is wet” because “it is raining” plus the rule “rain makes the ground wet”. Later you learn it is not raining after all. A plain forward chainer is now stuck: it already asserted “wet ground” and has no memory of why, so it cannot tell which conclusions to take back. You either keep a stale belief or throw everything away and re-derive from scratch.

A truth maintenance system (TMS) fixes this by separating two jobs:

The inference engine decides what to conclude (it runs the rules).
The TMS remembers why each conclusion holds and keeps the set of current beliefs consistent with those reasons as inputs change.

The justification-based TMS (JTMS) is the simplest member of this family, and it is the foundation that the rest of this codebase’s LTMS generalizes. Its whole job is to maintain a two-valued label, IN or OUT, over a network of nodes (propositions) connected by justifications (recorded inferences). A node is IN when it is currently believed and OUT when it is not.

The single most important thing to internalize, and the thing that trips up everyone porting or using a JTMS, is this:

OUT does not mean false. It means “not currently derivable”.

The JTMS can never conclude that something is false; it can only conclude that it has no reason to believe it right now. That is the defining limitation of the JTMS, and it is exactly the gap that the LTMS in ../src/ltms/core.py fills by adding a third label and real negation. Keep this contrast in your back pocket; it explains almost every design choice below.

Our JTMS lives in ../src/ltms/jtms.py, and a thin rule-engine wrapper (the “JTRE”) lives in ../src/ltms/jtre.py.

Concepts, step by step

Nodes

A Node is one proposition the system can believe or disbelieve. Each node carries:

a label (IN or OUT), cached so queries are instant;
a support, which records why the node currently holds (more on this below);
justs, the list of justifications that could make this node IN;
consequences, the justifications that use this node as an antecedent (so we know who to revisit when this node’s belief flips);
flags for whether it is an assumption and whether it is contradictory.

In the code, see the Node class around lines 74-119 of ../src/ltms/jtms.py.

Justifications

A Justification is a recorded inference of the shape

antecedents => consequence

Logically this is a definite (Horn) clause: “if all of these antecedents are believed, then believe the consequence.” Two special cases matter:

A justification with no antecedents is a premise: an unconditional belief, always IN, never retracted.
The set of justifications only ever grows. The JTMS never deletes a justification. Beliefs change by relabeling nodes, not by editing the rule network.

The three faces of `support`

This is the cleverest little piece of the data model, and worth slowing down for. A node’s support field answers “why do I currently believe this?” and it is overloaded three ways:

None – the node is OUT (no current support).
a Justification – the node is derived; if that justification has empty antecedents, the node is a premise.
the sentinel ENABLED_ASSUMPTION – the node is believed because we are currently choosing to assume it.

The support field always points at the node’s well-founded support: the one specific reason that is propping it up right now, not just any reason that could. This is what makes explanation cheap (why_node) and what makes retraction correct. See lines 37-46 and the _EnabledAssumption sentinel in ../src/ltms/jtms.py. The sentinel is compared by identity (is), which is why it is a singleton object rather than a string.

Assumptions

An assumption is a node you can switch on and off by hand. This is how the inference engine does hypothetical reasoning (“suppose it is raining…”).

convert_to_assumption marks a node as assumable.
enable_assumption switches it on: if the node was OUT, it becomes IN with support ENABLED_ASSUMPTION, and that IN-ness propagates forward.
retract_assumption switches it off again, which is where the interesting work happens.

There is a subtle precedence rule in enable_assumption (lines 194-204): if the node is already IN via a premise or a real justification, enabling it as an assumption leaves the stronger support alone. Exercise 1 is entirely about why that is the right call.

Adding belief: the monotone forward sweep

Anything that can only add belief, that is, asserting a new justification or enabling an assumption, is easy. The JTMS does a monotone forward sweep:

Check whether a justification is now satisfied: its consequence is currently OUT and all its antecedents are IN (_check_justification, _justification_satisfied, lines 215-220).
If so, install it as the consequence’s support and mark the consequence IN (_install_support, _make_node_in).
Then walk that node’s consequences and repeat, in a breadth-first queue (_propagate_inness, lines 226-234).

Because adding belief never takes anything away, no ordering subtleties arise. Belief only flows OUT -> IN, never the reverse, during this phase.

Removing belief: strictly two-phase retraction

Retraction is the hard case and the heart of the chapter. When you retract an assumption (or otherwise pull support out from under a node), you must do it in two strictly separated phases. Doing them in one interleaved pass is a real bug, not a style preference.

Phase 1 – propagate outness (_propagate_outness, lines 253-264). Walk forward from the retracted node and mark OUT every node whose current support runs through it. The key detail is the test conseq.support is j: identity, not “is there some justification that mentions this node”. We only take a node OUT if the justification we are walking is the exact one currently holding it up.

Phase 2 – find alternative support (_find_alternative_support, lines 266-273). Only after phase 1 is completely done, revisit every node we just took OUT and ask: does it have some other satisfied justification we can install instead? If so, re-derive it (which re-propagates inness).

Why must these be separate? Imagine two nodes that justify each other: B <= C and C <= B. Suppose both are currently IN only because of some assumption you are now retracting. If you interleaved “look for new support” into the take-it-out walk, you might re-justify B using C (still IN at that moment) and C using B, leaving both standing on each other with no real ground underneath. That is ill-founded circular support: a belief that holds only because it holds. The two-phase split forbids it: phase 1 takes both of them OUT first, so when phase 2 looks for support there is no phantom belief left to lean on. STUDY-NOTES.md (section 4) calls this out as “the bug the two-phase split exists to prevent”, and the same discipline reappears in the LTMS’s propagate_unknownness / find_alternative_support.

Contradictions: signal, do not resolve

A node can be flagged contradictory. The JTMS watches these: after any operation, check_for_contradictions (lines 277-282) looks for a contradictory node that is IN and, if it finds one, calls the contradiction handler.

Crucially, the JTMS only signals the conflict; it never fixes it. The default handler just raises JTMSContradiction. Deciding which assumption to back off (dependency-directed backtracking) is the inference engine’s job, and the JTMS supports that job with one introspection primitive:

assumptions_of_node (lines 286-300) walks the current well-founded support chain back to the enabled assumptions underneath a node. Those are the “culprits” an engine would consider retracting.

Two honest caveats, both of which become exercises:

assumptions_of_node returns the assumptions of one support (the installed one), not all possible ones and not a minimal set. That is Exercise 4.
The JTMS does nothing clever to avoid a doomed search; it discovers a contradiction only after relabeling its way into it. Caching “nogoods” to bail out early is Exercise 6.

Explanation

why_node (lines 305-315) turns the support field into a one-line explanation: OUT, or IN via an enabled assumption, or IN via a named justification with its antecedents listed, or IN as a premise. Because support always points at the real current reason, this is just a read; no search is needed. This is the payoff of maintaining well-founded support eagerly.

The examples, explained

The chapter’s runnable demonstrations live in ../exercises/ch07/solutions.py. Each is a small self-contained scenario built with the public API, and together they cover the JTMS behaviors that are easiest to see rather than just argue about.

`demo_jtre_belief_revision` – the canonical story

This is the “rain makes the ground wet” story end to end, run through the JTRE (the JTMS-backed rule engine):

e = JTre()
e.assume(("rain",), "user")                       # raining? assume so
e.justify("wet-rule", ("wet", "ground"), [("rain",)])
e.is_in(("wet", "ground"))   # True
e.why(("wet", "ground"))     # IN via wet-rule <= ('rain',)
e.retract(("rain",), "user")                       # never mind, not raining
e.is_in(("wet", "ground"))   # False  -- belief revised automatically

The point: nobody told the system to disbelieve “wet ground”. Retracting the only support (rain) caused phase-1 outness to ripple forward, and phase 2 found no alternative, so the derived fact correctly went OUT. That is belief revision for free, which is the entire reason a TMS exists.

`demo_enable_assumption_rule` – premises win (Exercise 1)

Here a node p is first made a premise (an antecedent-free justification), then also converted to an assumption and enabled. The demo confirms that p keeps its premise support (is_premise stays True) rather than being demoted to a bare assumption. The lesson, expanded under Exercise 1 below, is that premise support is stronger (unconditional, non-retractable) than assumption support, so overwriting it would be strictly worse.

`demo_assumptions_of_node_superset` – the set is not minimal (Exercise 4)

Node g has two justifications: g <= a, b and g <= c. With a, b, c all enabled, g’s installed support is whichever justification was added first (j1), so assumptions_of_node(g) reports ['a', 'b']. But c alone would also support g. So the reported set is not minimal, and the alternative support ({c}) is not even a subset of it. This demo makes the abstract caveat about assumptions_of_node concrete.

`demo_alternative_support_switch` – phase 2 in action (Exercise 4 support)

Node c is justified independently by a and by b. Before retraction, assumptions_of_node(c) names just a (the installed support). Retract a, and the demo shows c stays IN while assumptions_of_node(c) now names b. This is exactly _find_alternative_support doing its job: the belief survives because an independent reason remained, and the recorded support switched to it.

`demo_contradiction_and_culprits` – signal and blame (Exercise 6 context)

Two assumptions p and not-p jointly justify a contradictory node. Enable both and the contradictory node goes IN; the default handler raises JTMSContradiction; and assumptions_of_node on the contradictory node recovers the culprit set {p, not-p}. That culprit set is precisely the “nogood” an engine would record to avoid re-entering this conflict, which is the setup for Exercise 6.

Exercises walk-through

Full write-ups (paraphrased problem + answer) are in ../exercises/ch07/README.md. Several exercises ask you to modify the algorithm, so they are answered in prose; the behavior-probing ones are backed by code in ../exercises/ch07/solutions.py. Highlights:

Exercise 1 (why not let an assumption override existing support?). The proposed “improvement” has solidity backwards. A node already held by a justification or premise is supported by other beliefs and so is not retractable on its own. Overwriting that with ENABLED_ASSUMPTION would (a) hide the real reason from why_node/assumptions_of_node, (b) make a stable belief spuriously retractable, and (c) let you “retract” a premise that holds unconditionally. So keeping the existing support is correct. Demonstrated by demo_enable_assumption_rule.
Exercise 2 (propagate premise-hood to universally held nodes). A node justified entirely by premises holds universally but is not itself recorded as a premise. You can propagate the property: add a universal flag, seed it on premises, and when a justification fires whose antecedents are all universal, flag the consequent and give it a premise justification. The payoff is fewer wasted backtracks (such nodes get an empty assumptions_of_node). The cost is steep: you destroy retractability and counterfactual reasoning for those nodes, you collapse their explanations to a bare “premise”, and you take on cycle-guarding bookkeeping. A clear “you gain pruning, you lose flexibility” trade.
Exercise 3 (propagate contradiction-hood). Dual of Exercise 2: if a contradiction’s justification has all-but-one antecedents universally held, that last antecedent must itself be contradictory. Implementable as a fixpoint on top of the universal flag, with cycle guards. But it is only marginally useful in a pure JTMS, because a contradiction here merely signals the engine; the JTMS does not exploit the extra markings to prune anything. The idea pays off in richer systems (ATMS nogood minimization), foreshadowing later chapters.
Exercise 4 (assumptions-of-node is not minimal). Shown live by demo_assumptions_of_node_superset. The README also implements minimal_assumptions_of_node using the book’s retract-and-test hint: start from the reported set, try retracting each assumption, drop the ones the node survives without, restore the ones it needs. Note the demo’s striking result: starting from {a, b} the routine returns {}, because c was quietly supporting g the whole time. Part (c) shows you can have several equally small supporting sets ({c} or {d}), and part (d) explains why an engine wants the minimal set: smaller nogoods prune more general future contexts and avoid blaming irrelevant assumptions.
Exercise 5 (count-based justification satisfaction). Re-scanning every antecedent on every change is wasteful. Cache an out_count per justification (number of antecedents currently OUT); decrement on OUT -> IN, increment on IN -> OUT; a justification is satisfied exactly when the count hits zero. This turns the satisfaction check from O(antecedents) into O(1) per event. Correctness still rests on two-phase retraction (do all outness before any inness), so the count never declares a node supportable via something that depends on the node itself. This is the JTMS cousin of the LTMS counter trick in ../src/ltms/core.py.
Exercise 6 (cache nogoods to abort doomed relabeling). Keep a global list of minimal inconsistent assumption sets (nogoods). Before enabling an assumption, check whether the prospective enabled set would contain a known nogood; if so, skip relabeling entirely and signal a contradiction immediately. The README explains the subtle trap: just installing a contradictory justification for each bad set does not help, because that justification only fires after the JTMS has already done the full relabeling sweep to make those assumptions IN, which is exactly the work you wanted to skip. The cheap-subset-test look-ahead is the whole point. demo_contradiction_and_culprits shows recovering the very set you would store.
Exercise 7 (one-blocker-per-justification). Record, per justification, a single antecedent that is currently OUT (the “blocker”), and per node, the justifications it is blocking. A justification with a blocker is ignored; when a node goes IN, only revisit the justifications it was blocking and either re-watch a new blocker or fire. This is the truth-maintenance form of the two-watched-literal trick (the same idea the LTMS uses in ../src/ltms/watched.py). It wins big for high-fan-in, high-churn justifications and is a lazier, pointer-based cousin of Exercise 5’s counters.
Exercise 8 (derivation-depth scheme). Replace IN/OUT propagation with a per-node depth: the minimum over its justifications of 1 + max(depth of antecedents), with depth 0 for premises/assumptions and infinity for unsupported. A node is IN iff its depth is finite. This is a shortest-path computation on the justification DAG. Retraction with cycles still needs a two-phase shape (invalidate to infinity, then relax outward from the still-finite frontier) so that an ungrounded cycle cannot keep itself finite. The depth count is a bonus: shortest-proof explanation, search-cost estimation, cheap cycle detection, and tighter incremental update scoping.

Try it in this repo

All commands are run from the repository root. Activate the virtualenv first if you use one (. .venv/bin/activate).

Run the Chapter 7 exercise demonstrations (Exercises 1, 4, and 6 against the real JTMS, plus the end-to-end JTRE belief-revision demo):

python exercises/ch07/solutions.py

You will see, among other results, the belief-revision story and the non-minimal-assumptions phenomenon:

'jtre_belief_revision': {'wet_in_with_rain': True,
                         'why_wet': "('wet', 'ground') is IN via wet-rule <= ('rain',)",
                         'wet_in_after_retract_rain': False}
'ex4_assumptions_of_node_non_minimal': {'g_in': True,
                                        'current_support': 'j1',
                                        'assumptions_of_node_g': ['a', 'b'],
                                        'minimal_assumptions_of_node_g': []}

Explore the JTMS directly in a Python shell:

from ltms import JTMS

j = JTMS("demo")
rain = j.create_node("rain", assumption=True)
wet  = j.create_node("wet-ground")
j.justify_node("wet-rule", wet, [rain])   # rain => wet-ground

j.enable_assumption(rain)
print(wet.is_in)          # True
print(j.why_node(wet))    # wet-ground is IN via wet-rule <= rain

j.retract_assumption(rain)
print(wet.is_in)          # False  -- belief revised
print(j.why_node(wet))    # wet-ground is OUT.

A world model can also live in a data file, with no theory in the Python. The belief_revision.kb model encodes the same “two independent causes of wet ground” idea (two justifications, retract one cause, the other keeps the belief alive):

python examples/run_kb.py examples/kb/belief_revision.kb

which prints:

Loaded examples/kb/belief_revision.kb
  wet ground: true        # supported by rain
  wet ground: true        # rain retracted, sprinkler still supports it
  wet ground: unknown     # nothing supports it now

One honesty note: the .kb loader runs on the project’s LTMS-backed engine, not the bare JTMS, so it reports unknown where the pure JTMS would say OUT. The belief-revision behavior it shows, alternative support keeping a conclusion alive and the conclusion dropping when all support is gone, is exactly the JTMS idea of this chapter. For a run that exercises the JTMS layer specifically, stick with exercises/ch07/solutions.py and the JTre snippet above.

Takeaways

A JTMS separates deciding what to believe (the engine’s job) from tracking why, and keeping belief consistent (the TMS’s job).
IN/OUT is believed / not-currently-derivable, never true / false. The JTMS cannot represent or derive negation; that is the precise boundary the LTMS crosses.
support is the single source of truth for why a node holds: None, a Justification (empty antecedents = premise), or ENABLED_ASSUMPTION. Keeping it pointed at the real, well-founded reason is what makes explanation a free lookup.
Adding belief is an easy monotone forward sweep. Removing belief must be strictly two-phase (outness first, then look for alternative support) or you admit ill-founded circular support.
The JTMS only signals contradictions; backtracking is the engine’s job, bootstrapped by assumptions_of_node, which gives the assumptions behind one current support (not all, not minimal, by design).
The exercises sketch the standard performance and search refinements (satisfaction counters, watched-blocker pointers, nogood caching, premise/contradiction propagation, derivation-depth), most of which resurface, generalized, in the LTMS chapters that follow.