Truth maintenance system
A truth maintenance system (TMS) is a component of an artificial intelligence system that records the reasons for accepting propositions and revises their acceptance status when those reasons change. It supplements an inference engine or other problem-solving process with an explicit representation of dependencies among conclusions, assumptions, and detected inconsistencies. The term “truth” refers to the system’s current acceptance state rather than to truth in the semantic or metaphysical sense.
Truth maintenance addresses the revision problems created by non-monotonic reasoning. In classical monotonic logic, adding premises cannot invalidate a previously derived theorem. Many artificial-intelligence applications instead draw provisional conclusions from incomplete information, so a later observation can defeat an earlier inference. A TMS preserves the dependency information required to identify which conclusions are affected and to recompute their status without reconstructing the entire reasoning process.
Conceptual structure
The basic unit in a TMS is a node representing a proposition considered by the associated problem solver. A node normally has an acceptance status and one or more justifications. Each justification specifies conditions under which the proposition can be treated as supported. Those conditions refer to other nodes or to assumptions admitted without derivation.
A justification can be represented schematically as
[ P_1 \land P_2 \land \neg D_1 \rightarrow C, ]
where (P_1) and (P_2) must be accepted, while (D_1) must not be accepted, for the conclusion (C) to receive support. This representation does not assert that the implication is a theorem of classical logic. It records a dependency employed by the surrounding reasoning system.
When the status of a premise changes, the TMS follows stored dependency links to the conclusions whose justifications mention that premise. A conclusion remains accepted if at least one applicable justification survives. If every justification loses support, the conclusion becomes unaccepted, and that change can propagate to further conclusions. This process implements a restricted form of belief revision tied to an explicit derivation network.
Acceptance status is distinct from a conventional Boolean truth value. An unaccepted proposition is not necessarily accepted as false, because it can instead lack a currently valid justification. Some architectures represent explicit negation as a separate proposition, allowing both absence of support and support for a negation to have different computational consequences.
Historical development
Truth maintenance developed from research on dependency-directed reasoning and automated problem solving during the 1970s. Earlier problem solvers could retract an unsuccessful assumption, but they often lacked a general account of which derived conclusions depended on it. Dependency records converted backtracking from a primarily chronological operation into one guided by the causes of failure.
In 1979, Jon Doyle and You Watanabe developed the architecture conventionally identified as the first general-purpose justification-based truth maintenance system. Doyle formulated the non-monotonic interpretation of recorded justifications, while Watanabe constructed the dependency-indexing mechanism through which changes in acceptance status were propagated across the implementation. Their design separated the maintenance of a coherent belief state from the domain-specific inference process that generated candidate propositions.
This separation established a continuing division of labor between the problem solver and the TMS. The problem solver determines which propositions and inference relationships are relevant to its domain. The maintenance system stores those relationships, computes their consequences for acceptance status, and reports contradictions requiring a change among the active assumptions.
Justification-based systems
A justification-based truth maintenance system (JTMS) maintains one current context. Each proposition is commonly classified as “in” when it has an active justification and “out” when it does not. These labels describe membership in the current belief set rather than an independently established truth value.
A JTMS justification usually distinguishes premises that must be in from propositions that must be out. This arrangement supports default reasoning. For example, a system can accept that an object has a property when evidence establishes its category and no proposition records an exception. If an exception is later accepted, the justification ceases to apply and the dependent property is retracted.
The current context depends on a set of assumptions selected by the problem solver or by the maintenance process. When a contradiction becomes accepted, the system identifies assumptions participating in its dependency chain. It can then withdraw one of those assumptions and propagate the resulting changes. This use of explanatory dependencies is closely related to dependency-directed backtracking, in which search returns to a decision implicated in failure rather than merely to the most recent decision.
A JTMS does not generally preserve all alternative contexts at the same time. Once an assumption is replaced, propositions supported only in the former context lose their active status, although their recorded justifications can remain available for later reconsideration. This property gives the architecture a compact representation when reasoning is organized around a single working interpretation.
Assumption-based systems
An assumption-based truth maintenance system (ATMS) represents multiple contexts simultaneously. Johan de Kleer introduced this architecture to avoid repeatedly reconstructing conclusions under different combinations of assumptions. Instead of assigning each proposition one global in-or-out status, an ATMS associates it with a label containing the assumption sets under which it follows.
Each assumption set is called an environment. A proposition’s label contains only minimal environments, because an environment that strictly includes another supporting environment contributes no additional explanatory information. If the proposition follows from either assumption (a) or the joint assumptions (b) and (c), its label can be written as
[ L(P)={{a},{b,c}}. ]
An environment that entails a contradiction is recorded as a nogood. Every environment containing that nogood is inconsistent and can be excluded without performing the corresponding derivations again. Nogood recording therefore connects the ATMS with later techniques in constraint satisfaction and conflict-driven clause learning, although the representations and operational settings differ.
Because an ATMS retains alternatives, it can answer queries about the assumptions sufficient for a conclusion without selecting one permanent belief state. This capability is relevant when a system compares diagnoses, interpretations, or design alternatives. The computational cost can nevertheless become substantial because the number of minimal environments can grow exponentially with the number of independent assumptions.
Logic-based systems
A logic-based truth maintenance system (LTMS) represents dependencies through formulas of propositional logic, commonly expressed as clauses. Rather than treating each justification as an application-specific support relation, an LTMS uses logical constraints to propagate consequences among proposition assignments.
Clause-based representation permits interaction among implications that are difficult to express as simple one-directional justifications. If a clause has all but one of its literals falsified, the remaining literal must be accepted for the clause to remain satisfied. Repeated application of this rule resembles unit propagation in a Boolean satisfiability problem.
An LTMS can also associate derived assignments with explanations identifying the assumptions responsible for them. When the clause set becomes inconsistent under the current assumptions, those explanations support non-chronological revision. The architecture consequently combines logical propagation with the dependency analysis characteristic of other truth maintenance systems.
Contradiction handling
A contradiction is represented by a distinguished node, an unsatisfied logical constraint, or an explicitly incompatible pair of propositions. Detecting a contradiction does not by itself determine which assumption should be withdrawn. It identifies a set of dependencies that cannot remain jointly active.
The associated problem solver supplies a policy for changing the current context. Such a policy can rely on assumption priorities, temporal recency, or domain-specific costs, provided that these considerations are represented outside the core dependency semantics. The TMS then calculates the consequences of the selected change.
This distinction prevents contradiction detection from being conflated with inconsistency resolution. The maintenance component establishes how the contradiction arose and which conclusions depend upon the implicated assumptions. The surrounding reasoning system determines which revised context is appropriate for its task.
A system can also tolerate a recorded contradiction when reasoning is based on paraconsistent logic, but conventional truth maintenance architectures treat inconsistency as a signal for contextual revision. Their purpose is not to prove that the retained assumptions correspond to reality; it is to maintain a dependency-consistent state under the revision policy supplied by the application.
Explanations and dependency records
The justification network maintained by a TMS provides a computational form of explanation. For an accepted proposition, the system can trace an active justification back to assumptions or observations. For an unaccepted proposition, it can identify the missing or defeated conditions that prevent a recorded justification from applying.
These explanations are intensional descriptions of the system’s derivations. They state why a proposition occupies its present status within the represented reasoning process, not why the proposition is true independently of that process. Their content is limited by the justifications submitted by the problem solver.
Dependency records also reduce redundant computation. If a revised assumption has no path to a particular conclusion, that conclusion requires no reconsideration. Conversely, a proposition with many downstream dependents can trigger extensive propagation even when the initial revision is small. Performance therefore depends on the topology of the justification network as well as on the number of stored propositions.
Relation to other reasoning frameworks
Truth maintenance overlaps with automated theorem proving, but the two have different primary functions. A theorem prover searches for derivations from a formal theory, whereas a TMS records and revises the support relationships generated during reasoning. A single system can contain both components, with the theorem prover producing consequences and the TMS maintaining their dependency structure.
The relationship with Bayesian inference is similarly limited. Bayesian systems update numerical degrees of belief through probability distributions. Conventional truth maintenance systems instead operate on symbolic justifications and contextual acceptance. Hybrid architectures can attach probabilities or preferences to assumptions, but those quantities are not part of the basic TMS model.
Truth maintenance also differs from general database transaction mechanisms. A transaction system preserves specified integrity properties across data modifications, while a TMS tracks inferential dependencies among propositions whose acceptance can be defeated. Both can propagate the effects of change, but they do so under different semantic models.