A truth maintenance system (TMS) is a mechanism whereby a knowledge-based system such as Cyc can remain consistent and truthful as its knowledge changes. For example, if facts have been added to the KB through inference based on a set of premises, and one of the premises is later removed from the KB, any conclusion that depends on that premise should also be removed from the KB. The Cyc TMS relies on the fact that each assertion has all of its arguments recorded in the data structure.
When a Deduction is added to the KB, TMS records the list of Supports that can be used to re-justify the deduction. Some supports are just GAF or rule assertions from the KB. However, some are complex objects called HL supports, which “package up” particular truths that can be verified by dedicated HL Modules. Oftentimes, TMS will eagerly re-evaluate the supports for a deduction to determine if it should stay in the Knowledge Base. However, some HL supports (e.g., :QUERY) are only re-evaluated when a user performs a “Redo TMS” operation on the deduction. In this respect, TMS can behave “lazily” for some types of HL supports.