justification-propagation

70 beliefs (59 IN, 11 OUT)

Justification propagation is the central mechanism by which a Truth Maintenance System keeps its belief network consistent as knowledge changes. This topic covers how truth values are computed, how changes ripple through dependency chains, and what guarantees the system provides about correctness and termination. It matters because every higher-level TMS operation — retraction, challenge, supersession, dialectical reasoning — ultimately bottoms out in justification evaluation and propagation.

The foundational semantics are clean and minimal. A justification is valid when all its antecedents are IN and all its outlist nodes are OUT (justification-validity-requires-inlist-in-and-outlist-out). A node is IN when any of its justifications is valid — disjunction across justifications, conjunction within each one (sl-justification-semantics, node-in-if-any-justification-valid, network-disjunctive-justification). This means adding a justification can never cause a node to go OUT (node-truth-disjunctive). Evaluation is pure with no side effects (justification-valid-is-pure), uniform across SL and CP types which share the same validity check (cp-and-sl-evaluated-identically), and context-independent — when a justification is attached has no bearing on the result (justification-timing-is-irrelevant-to-evaluation, justification-evaluation-is-context-independent). Premise behavior emerges naturally from these rules: a node with no justifications defaults to IN, and empty antecedent lists are vacuously valid (premise-behavior-emerges-from-absence, premise-defaults-to-in, empty-antecedents-vacuously-valid). A notable asymmetry exists in how missing nodes are handled: absent antecedents fail validation conservatively, while absent outlist nodes pass permissively, enabling "believe X unless Y" patterns where Y may not yet exist (missing-nodes-have-asymmetric-fail-semantics, sl-outlist-asymmetry).

Propagation itself uses BFS through a dependents index (propagation-is-bfs), with several interlocking guarantees. It terminates deterministically because BFS prevents stack overflow, stop-on-unchanged prevents oscillation, and the cascade selectively follows only paths where truth values actually change (propagation-terminates-deterministically, propagate-cascade-stops-on-unchanged). It is lifecycle-safe, skipping retracted nodes that are pinned OUT via metadata (propagate-skips-retracted-nodes, retracted-pin-survives-recompute), and the trigger node is never recomputed by propagation itself — callers must set its value first (propagate-does-not-change-trigger). The system handles graph inconsistencies gracefully, skipping dangling references with warnings rather than crashing (propagation-is-safe-under-graph-inconsistency). When adding a justification to an existing node, propagation is multi-dimensional: truth values cascade through dependents, the reverse index is updated on both antecedent and outlist nodes, and access tags recompute transitively (add-justification-is-fully-propagating, add-justification-registers-dependents, add-justification-propagates-tags-downstream). Retraction cascades are transitive and terminating, with the system computing surgical restoration hints that target only cascade victims with surviving premises, excluding the directly retracted node (retraction-cascade-is-transitive-and-terminating, restoration-hints-are-surgical, hints-exclude-directly-retracted-node).

Several beliefs in this topic are OUT, reflecting refined understanding over time. The belief that propagation automatically cascades on all truth changes including outlist-mediated ones was retracted (propagation-automatically-cascades-on-all-truth-changes), as were several beliefs about premise identity transformation (premise-identity-is-inherently-transient, premise-identity-is-bidirectionally-transformable, premise-identity-transformation-is-architecturally-asymmetric) — suggesting that earlier claims about how premise status changes were superseded or found to be inaccurate. The retraction of propagate-assumes-dependents-exist indicates the system evolved from crashing on dangling references to handling them gracefully. Similarly, several reporting-related beliefs were retracted (removal-effects-are-fully-reported-and-recoverable, retraction-reporting-reflects-complete-cascades), likely because the completeness guarantees they claimed were found to depend on conditions not always met. The retraction of truth-evaluation-is-transformation-invariant and richer-revision-preserves-evaluation-invariance suggests that while evaluation is pure in isolation, broader claims about invariance across all structural transformations did not hold up under scrutiny.

IN add-justification-achieves-consistent-propagation
Adding a justification to an existing node produces a fully consistent network state through guaranteed-terminating multi-dimensional propagation: truth values cascade via BFS through dependents, the reverse index is updated, and access tags recompute transitively — all within a single operation whose termination is guaranteed by BFS traversal and stop-on-unchanged semantics.
IN add-justification-is-fully-propagating
Adding a justification triggers complete multi-dimensional propagation: truth values cascade through dependents via BFS, the dependents reverse index is updated on both antecedent and outlist nodes, and access tags flow downstream transitively through all dependent chains.
IN add-justification-propagates-tags-downstream
Calling `add_justification` on an existing node recomputes `access_tags` for the target and all its transitive dependents, enabling retroactive tag propagation.
IN add-justification-registers-dependents
`add_justification` updates the `dependents` set on both antecedent and outlist nodes so that future retraction/restoration propagation reaches the target node.
IN add-justification-returns-change-dict
`Network.add_justification` returns a dict with keys `node_id`, `old_truth_value`, `new_truth_value`, and `changed` (list of all nodes whose truth value changed).
IN add-justification-triggers-propagation
Adding a justification that changes a node's truth value triggers BFS propagation that cascades to all transitive dependents, including restoring OUT nodes whose justifications become valid.
IN add-node-evaluates-justification-at-insertion
When `add_node` is called with justifications, the node's initial truth value is computed immediately from the current state of its antecedents — a derived node added when its antecedent is OUT starts OUT
IN cp-and-sl-evaluated-identically
CP and SL justifications use the same validity check in `_justification_valid`; the distinction is semantic (support vs. consistency), not computational.
IN cp-equals-sl
CP (conditional-proof) justifications are evaluated with the exact same logic as SL justifications, despite being a distinct type in Doyle's TMS — either an intentional simplification or incomplete implementation
IN empty-antecedents-vacuously-valid
An SL justification with an empty antecedent list is valid (vacuous truth via `all([])`), allowing outlist-only justifications to function as "IN unless Y" — used by `challenge` and `supersede` for converted premises
IN hints-exclude-directly-retracted-node
The node passed to `retract_node` never appears in the `restoration_hints` list — only cascade victims with surviving premises do.
IN incremental-propagation-is-fully-complete
Incremental truth propagation reaches every node whose truth value should change — including nodes that depend via outlist entries — without requiring periodic full recomputation, because safe terminating BFS traversal operates over a dependents index that tracks both antecedent and outlist relationships.
IN justification-addition-is-robust-across-graph-states
Adding a justification to an existing node achieves fully consistent multi-dimensional propagation — truth values, dependents index, and access tags — even when the dependency graph contains dangling references or lifecycle-marked nodes, because propagation safely handles both graph anomalies and node lifecycle states.
IN justification-evaluation-is-context-independent
Justification evaluation produces identical results regardless of evaluation context: it is pure (no side effects), uniform across types (SL/CP use the same validity rule), and temporally invariant (attaching a justification at creation or later yields the same truth outcome) — making truth computation fully context-free
IN justification-evaluation-is-uniform-and-pure
All justification types (SL and CP) use the same validity rule (antecedents IN, outlist OUT), evaluated as a pure function with no side effects
IN justification-timing-is-irrelevant-to-evaluation
Justification evaluation produces identical truth semantics regardless of when a justification is attached: add_node evaluates justifications immediately at insertion, and add_justification triggers identical propagation when attached post-creation — the system has no time-of-attachment sensitivity.
IN justification-valid-is-pure
`_justification_valid` is a pure query with no side effects, no logging, and no mutations to network state
IN justification-validity-requires-inlist-in-and-outlist-out
A justification is valid iff all antecedents are IN and all outlist nodes are OUT; this single rule drives retraction cascades, kill-switch behavior, challenges, and supersession
IN missing-nodes-have-asymmetric-fail-semantics
Missing nodes are treated asymmetrically: absent antecedents fail validation (conservative), absent outlist nodes pass (permissive), creating a "believe unless proven otherwise" default
IN missing-outlist-nodes-pass-validation
In `_justification_valid`, missing antecedent nodes cause the check to fail (node goes OUT), but missing outlist nodes pass (don't block) — an open-world default.
IN network-disjunctive-justification
A node is IN if ANY of its justifications is valid (disjunction); each individual justification requires ALL antecedents IN and ALL outlist members OUT (conjunction) — the SL justification semantics from Doyle's 1979 paper.
OUT network-is-sole-truth-propagation-engine
All truth value computation and propagation in the system flows through `Network._propagate()` and `Network._compute_truth()`; no other module modifies truth values directly.
IN network-single-justification-removal-blocked
`remove_justification()` raises `ValueError` when a node has exactly one justification, forcing callers to use `convert_to_premise` or `retract` instead — preventing accidental creation of unjustified non-premise nodes.
IN node-in-if-any-justification-valid
A Node is IN when at least one of its Justifications is valid; a Justification is valid when all antecedents are IN and all outlist nodes are OUT (disjunctive over justifications, conjunctive within each).
IN node-truth-disjunctive
A node is IN if ANY of its justifications is valid (disjunctive semantics); adding a justification to a node can never cause it to go OUT.
IN premise-behavior-emerges-from-absence
Premise behavior is not explicitly implemented — it emerges from three defaults: nodes with no justifications default to IN, empty antecedent lists are vacuously valid, and the system preserves a premise's current truth value rather than deriving it.
IN premise-can-receive-justification
A premise node (initially no justifications) can receive a justification via `add_justification`, giving it a derived backup path that keeps it IN even if its premise status is retracted.
IN premise-count-is-per-justification-max
`premise_count` in the return value reports the maximum antecedent count across the node's justifications, not the total across all justifications (any_mode with 3 premises returns 1, not 3).
IN premise-defaults-to-in
A node with no justifications (a premise) defaults to IN; `_compute_truth` preserves its current truth value rather than recomputing it.
OUT premise-identity-is-bidirectionally-transformable
Premise identity can be both destroyed (via dialectical challenge adding justifications) and created (via convert-to-premise removing them), with both directions preserving the dependents invariant — making premise/derived status a fully reversible structural property of the network.
OUT premise-identity-is-inherently-transient
Premise identity is inherently transient because it emerges from the absence of justifications, and any justification addition — whether from dialectical challenge, defend, or direct add_justification — irreversibly transforms a premise into a derived node without explicit opt-in.
OUT premise-identity-transformation-is-architecturally-asymmetric
Premise identity transformation exhibits a fundamental architectural asymmetry rooted in the same emergent property: premise identity is inherently transient because it arises from the absence of justifications, and dialectical challenge exploits this transience to permanently transform premises into justified nodes — while the truth-value defeat itself remains fully reversible through outlist semantics, creating an irreversible identity change layered atop reversible truth dynamics
IN premises-have-no-justifications
A premise node is represented by an empty `justifications` list and defaults to `truth_value="IN"`; the system treats the empty-justifications case as a special unconditional belief.
OUT propagate-assumes-dependents-exist
Every ID in `node.dependents` is accessed via `self.nodes[dep_id]` without a membership check; a dangling dependent reference will raise `KeyError` — this is intentional (broken invariant = bug)
IN propagate-cascade-stops-on-unchanged
If a dependent's recomputed truth value equals its current value, it is not enqueued — the cascade terminates along that path, making propagation selective rather than exhaustive
IN propagate-does-not-change-trigger
The seed node (`changed_id`) is added to `visited` immediately and never has its own truth value recomputed; callers must update it before calling `_propagate`
IN propagate-skips-retracted-nodes
`_propagate` never recomputes truth values for nodes with `_retracted` in metadata, even if their justifications would support IN; only `assert_node` can restore them
OUT propagation-automatically-cascades-on-all-truth-changes
Truth propagation automatically cascades to all dependent nodes whenever any node's truth value changes, including nodes that appear only in outlists — making GATE belief re-evaluation fully automatic with no manual intervention required after outlist node retraction.
IN propagation-is-bfs
Truth value propagation in `_propagate` uses `deque`-based BFS through the `dependents` graph, not DFS, ensuring breadth-first wavefront expansion.
IN propagation-is-crash-free
Truth propagation completes without runtime errors across all reachable nodes
IN propagation-is-safe-and-terminating
Truth propagation is both lifecycle-safe and guaranteed to terminate: retracted nodes are skipped, trigger nodes are never recomputed, BFS prevents stack overflow, and stop-on-unchanged prevents oscillation — propagation respects every node state it encounters.
IN propagation-is-safe-under-graph-inconsistency
Truth propagation achieves correctness even when the dependency graph contains dangling references: missing nodes are skipped with structured warnings rather than crashing, dangling IDs are excluded from both the changed and visited sets, and this graceful degradation composes with the underlying termination and lifecycle-awareness guarantees for all reachable nodes.
IN propagation-is-topology-complete-and-inconsistency-safe
Truth propagation is both topologically complete — reaching all transitively dependent nodes including those connected through outlist entries, not just antecedent references — and safe under graph inconsistency, skipping dangling dependent references with structured warnings rather than crashing, ensuring correct cascading even in networks with imperfect structural integrity such as nodes deleted without full reference cleanup.
IN propagation-respects-node-lifecycle
Truth propagation respects node lifecycle states: retracted nodes are skipped during BFS traversal, and the trigger node itself is never recomputed — callers must set its truth value before invoking propagation.
IN propagation-terminates-deterministically
Truth propagation is guaranteed to terminate: BFS prevents stack overflow, stop-on-unchanged prevents oscillation, and fixpoint iteration bounds the outer loop
OUT removal-effects-are-fully-reported-and-recoverable
Every belief removal — whether intentional retraction or contradiction-triggered backtracking — provides three simultaneous guarantees: complete cascade coverage (transitive propagation captures every truth-value change), accurate effect reporting (structured before/after diffs reflect all affected nodes), and surgical recovery guidance (restoration hints target only cascade victims with surviving premises).
IN remove-justification-enforces-minimum-count
`Network.remove_justification` refuses to remove the last justification from a derived node — a derived node must retain at least one justification, enforced with `ValueError("only one justification")`
IN restoration-hints-are-surgical
Restoration hints provide surgical recovery guidance after retraction cascades: hints exclude the directly retracted node (targeting only cascade victims) and require at least one surviving premise in a multi-premise justification — narrowing recovery scope to nodes that can actually be independently re-justified.
IN restoration-hints-require-surviving-premises
A retraction cascade only produces a `restoration_hint` for a node if it has a multi-premise SL justification and at least one of its premises is still IN after the cascade.
IN retract-computes-restoration-hints
`retract_node` computes `restoration_hints` by examining surviving premises of multi-antecedent justifications, enabling callers to identify which premises could rebuild retracted derived beliefs.
IN retract-returns-changed-set
`Network.retract()` returns a list of all node IDs whose truth value changed, including the target and all transitively affected dependents; retracting an already-OUT node returns `[]`
IN retracted-nodes-skipped-in-propagation
Retracted nodes (marked with `_retracted` metadata) are skipped during BFS propagation but remain in the network for potential restoration.
IN retracted-pin-survives-recompute
A node explicitly retracted via `retract()` gets a `_retracted` metadata flag that pins it OUT — surviving both `assert_node` on its antecedents and `recompute_all()`, clearable only by `assert_node` on the pinned node itself
IN retraction-cascade-is-transitive-and-terminating
Retraction cascades are both transitive in reach (propagating OUT to all transitively dependent SL-derived nodes, not just direct children) and guaranteed to terminate safely (BFS prevents oscillation, retracted nodes are skipped, and the cascade stops when no truth values change) — ensuring thorough impact without risk of runaway propagation.
OUT retraction-effects-are-reported-with-recovery-guidance
Every retraction provides both complete effect reporting (structured before/after diffs for all mutating operations, full changed set) and surgical recovery guidance (restoration hints targeting only cascade victims with surviving premises, excluding the directly retracted node), giving callers full situational awareness and actionable recovery paths from a single operation.
OUT retraction-reporting-reflects-complete-cascades
The retraction reporting system provides accurate effect coverage across all cascade paths — structured before/after diffs capture every truth-value change, restoration hints target only cascade victims with surviving premises, and the cascade itself transitively reaches all dependent nodes — but only when the dependents index tracks all relationship types including outlists, ensuring no outlist-mediated cascade victims produce unreported effects.
OUT richer-revision-preserves-evaluation-invariance
Although the revision system governs state richer than binary truth values — including metadata-enabled lifecycle governance with retraction reasons, staleness indicators, and access controls — truth evaluation remains transformation-invariant, producing identical results regardless of attachment history or structural origin; the richer governance layer operates orthogonally to evaluation, enriching management capabilities without compromising core determinism.
IN sl-conjunction-any-disjunction
Covered by existing `sl-justification-semantics`, `truth-is-disjunctive-over-conjunctive-rules`, and `node-in-if-any-justification-valid`
IN sl-justification-is-disjunctive
A node is IN if *any* of its justifications is valid (disjunctive semantics); `_compute_truth()` short-circuits on the first valid justification rather than requiring all justifications to hold.
IN sl-justification-semantics
An SL justification is valid iff ALL antecedents are IN AND ALL outlist nodes are OUT; a node is IN iff ANY of its justifications is valid (conjunction within a justification, disjunction across justifications).
IN sl-outlist-asymmetry
Missing antecedents invalidate a justification, but missing outlist nodes do not — this asymmetry enables "believe X unless Y" where Y may not yet exist in the network
IN sl-param-is-comma-separated-node-ids
`add_node()` encodes SL justifications as comma-separated node IDs in the `sl=` parameter and outlist nodes in `unless=`, mirroring the TMS (SL, OL) formalism directly in the API signature.
IN sticky-retraction-survives-recompute-all
A node with `_retracted` metadata stays OUT even when `recompute_all()` re-evaluates the entire network — sticky retraction is a durable pin that only `assert_node` can clear
IN system-semantics-are-minimal-and-complete
The entire TMS — both monotonic truth maintenance and non-monotonic defeat — derives from a minimal set of uniform primitives: emergent truth rules (disjunction over conjunction, premise-from-absence) combined with a single reversible outlist mechanism that underlies all defeat features, with no additional machinery required.
IN tms-core-is-deterministic-and-conservative
The TMS engine produces deterministic, terminating truth maintenance through uniform pure evaluation, guaranteed convergence, and conservative asymmetric failure semantics for missing nodes.
OUT truth-evaluation-is-transformation-invariant
Truth evaluation produces identical results regardless of both temporal context (when a justification was attached — at node creation vs. later addition) and structural transformation (premise → justified node via challenge) — all forms of node history and identity change are invisible to the evaluation function, making truth a pure function of current network state.
IN truth-is-disjunctive-over-conjunctive-rules
A node's truth is a disjunction over justifications (any valid justification makes it IN), where each justification is a conjunction (all antecedents IN and all outlist OUT), and any-mode explicitly reifies OR semantics as per-premise justifications.
IN truth-semantics-are-emergent-and-uniform
Truth maintenance semantics are fully emergent from simple uniform rules: premise behavior arises from empty justification lists, evaluation is pure and type-agnostic across SL/CP, and node truth is a clean disjunction-of-conjunctions — no special cases exist anywhere in the evaluation path.
IN verify-dependents-is-read-only
`Network.verify_dependents()` never modifies the dependents index; it returns a list of human-readable error strings without side effects
IN verify-dependents-is-readonly
`verify_dependents()` never modifies `node.dependents`; it only reads and reports discrepancies as a list of human-readable strings containing `"extra"` or `"missing"`.