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
⊥	U+22A5	Up tack / Contradiction	The distinguished inconsistent node
∪	U+222A	Union	Label collects the environments that support a node
{	U+007B	Left curly bracket	Opens an in-list, out-list or environment
}	U+007D	Right curly bracket	Closes an in-list, out-list or environment
₁	U+2081	Subscript one	First element of an in-list or out-list
ᵢ	U+1D62	Latin subscript small letter i	Index over the in-list
ₙ	U+2099	Latin subscript small letter n	Last element of the in-list
ⱼ	U+2C7C	Latin subscript small letter j	Index over the out-list
ₘ	U+2098	Latin subscript small letter m	Last element of the out-list
a	U+0061	Latin small letter a	Node that must be believed for the justification to be valid
b	U+0062	Latin small letter b	Node that must not be believed
J	—	Justification	Pair of an in-list and an out-list
IN	—	Node status	Believed: some justification is valid
OUT	—	Node status	Not believed: no justification is valid
Label	—	ATMS label	Minimal environments supporting a node
nogood	—	Nogood	Environment shown to be inconsistent
n	—	Node	Belief tracked by the network

Metatheory. Doyle's system was an algorithm before it was a logic, and the reconstruction came a decade later. Elkan (1990) showed that the admissible labellings of a JTMS are exactly the stable models of the program obtained by reading in-lists as positive body literals and out-lists as negation as failure, and proved that deciding whether a network has such a labelling is NP-complete, so the algorithm's occasional failure to settle reflects genuine hardness rather than an implementation defect. The same correspondence identifies the failure case: a justification whose out-list contains its own node is the network form of a rule deriving a from not a, and it admits no labelling at all. Networks with empty out-lists are monotone and can be labelled in linear time by Horn propagation. For the ATMS, de Kleer (1986) defined the label of a node as the set of minimal consistent environments supporting it, which makes labelling a prime-implicant computation; a label can be exponentially large in the number of assumptions, so the cost lies in the output rather than in the search.

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

Limitations. A truth maintenance system records how beliefs depend on one another; it does not decide what to believe. When a contradiction is traced back, which assumption to retract is settled by the search order rather than by any principle in the system, so dependency-directed backtracking is not belief revision and answers to none of the AGM postulates. Non-monotonicity enters through out-lists and brings its failure cases with it: an odd loop through an out-list leaves the network with no admissible labelling, and deciding whether one exists is NP-complete. Where several labellings exist the system reports one, selected by the order in which justifications were installed, so the answer depends on history rather than content. The ATMS avoids that choice by carrying every environment at once, with labels exponential in the number of assumptions. Justifications are propositional and ground, so a rule must be instantiated before it can be recorded.