Truth-Maintenance Procedure
Invoked whenever a justification is added to a node.
1. Add the new justification to the node's justification set and update consequences of the nodes mentioned in the justification
2. Check consequences of the node. If there are none, set the node to IN and construct the IN and OUT lists. Otherwise, build a new list L containing the node and its repercussions, record the IN/OUT state of each node in L, and mark them temporarily with
3. For each node N of L, try to find a well-founded valid justification that will make it IN. If none can be found, mark it OUT. Either way, propagate any change in N's status to its consequences.
4. If a node in L is IN and it corresponds to a contradiction, than call the dependency-directed backtracking (DDB) procedure. If the truth maintenance procedure is activated during backtracking, repeat this step until no more contradictions are present (
5. Compare the current status of each node in L with its recorded status, and alert the user to changes in status.