Truth Maintenance Systems

Origin. Doyle (1979). Track belief dependencies. Reason maintenance under updates. ATMS: assumption-based (de Kleer 1986). JTMS: justification-based. Foundation for belief revision.

Models. Beliefs justified by other beliefs. Dependency network. Non-monotonic: beliefs can be retracted. Efficient update propagation. Multiple belief contexts.

Formalism.

JTMS (Justification-based): Nodes: beliefs/propositions. Justifications: J = (in-list, out-list). Node believed iff some justification valid.

Justification validity: J = ({a₁,...,aₙ}, {b₁,...,bₘ}) valid iff all aᵢ believed and all bⱼ not believed.

Node states: IN: believed (valid justification exists) OUT: not believed (no valid justification)

Dependency-directed backtracking: Contradiction found. Trace dependencies to assumptions. Retract minimal set.

ATMS (Assumption-based): Multiple contexts simultaneously. Environment: set of assumptions. Label(n): minimal environments supporting n.

ATMS propagation: Label(n) = ∪{envs supporting n via justifications} Minimal: no superset in label.

Nogood: Environment containing contradiction. Prune from all labels.

Default reasoning: Assumptions as defaults. Context: consistent assumption set. Multiple extensions possible.

Symbols.

Symbol	Unicode	Name	Meaning
IN/OUT	—	Status	Belief state
J	—	Justification	Support
⊥	U+22A5	Contradiction	Inconsistency
nogood	—	Nogood	Bad assumption set
label	—	Label	Supporting envs

Metatheory. Polynomial update for JTMS (well-founded). ATMS exponential worst case. Completeness for defaults. Sound constraint propagation.

Applies to. Expert systems. Diagnosis. Configuration. Planning. Nonmonotonic reasoning.

Limitations. Worst-case exponential. Many environments in ATMS. Integration with inference engines. Justification loops.