Problem Solving and Truth Maintenance Systems

Last Modified:

Introduction

 Truth Maintenance Systems (TMS), also called Reason Maintenance Systems, are used within Problem Solving Systems, in conjunction with Inference Engines (IE) such as rule-based inference systems, to manage as a Dependency Network the inference engine's beliefs in given sentences. 

		    PROBLEM SOLVING SYSTEM
	+--------------------------------------------+
	|					     |
	|	+----+	                +-----+	     |
	|	| IE |<---------------->| TMS |	     |
	|	+----+	                +-----+	     |
	|					     |
	+--------------------------------------------+
A TMS is intended to satisfy a number of goals:

Provide justifications for conclusions

When a problem solving system gives an answer to a user's query, an explanation of the answer is usually required. If the advice to a stockbroker is to invest millions of dollars, an explanation of the reasons for that advice can help the broker reach a reasonable decision.
An explanantion can be constructed by the IE by tracing the justification of the assertion.

Recognise inconsistencies

The IE may tell the TMS that some sentences are contradictory. Then, if on the basis of other IE commands and of inferences we find that all those sentences are believed true, then the TMS reports to the IE that a contradiction has arisen. For instance, in the ABC example the statement that either Abbott, or Babbitt, or Cabot is guilty together with the statements that Abbott is not guilty, Babbitt is not guilty, and Cabot is not guilty, form a contradiction.
The IE can eliminate an inconsistency by determining the assumptions used and changing them appropriately, or by presenting the contradictory set of sentences to the users and asking them to choose which sentence(s) to retract.

Support default reasoning

In many situations we want, in the absence of firmer knowledge, to reason from default assumptions. If Tweety is a bird, until told otherwise, we will assume that Tweety flies and use as justification the fact that Tweety is a bird and the assumption that birds fly.

Remember derivations computed previously

In the process of determining what is responsible for a network problem, we may have derived, while examining the performance of a name server, that Ms.Doe is an expert on e-mail systems. That conclusion will not need to be derived again when the name server ceases to be the potential culprit for the problem and we examine instead the routers.

Support dependency driven backtracking

The justification of a sentence, as maintained by the TMS, provides the natural indication of what assumptions need to be changed if we want to invalidate that sentence.
Our belief [by "our belief" we mean the "inference-engine's belief"] about a sentence can be:

We say a sentence in in if true or assumed-true; it is out if false, assumed-false, or don't-care.

A TMS maintains a Dependency Network. The network is bipartite, with nodes representing sentences and justifications.
A sentence may correspond to a fact, such as "Socrates is a man", or a rule, such as "if ?x is a man then ?x is mortal". We will say that a sentence node is a premise if its sentence is true, is a contradiction if its sentence is false, is an assumption if its sentence is assumed-true or assumed-false or assumed.
A sentence node receives arcs from justification nodes. Each such justification node provides an argument for believing the given sentence node. In turn a sentence node has arcs to the justification nodes that use it as a premise.

A justification node has inputs from sentence nodes, its premises or justifiers, and has output to a sentence node, its conclusion or justificand. A justification node represents the inference of the conclusion from the conjunction of the stated premises.

The conventions used in representing graphically dependency networks are summarized here.

The TMS maintains the following information with each sentence node:

The TMS maintains very little information with justification nodes. Only a label with value IN or OUT depending if we believe the justification valid or not.

The IE can give at least the following orders to the TMS:

Truth Maintenance Systems can have different characteristics:

Justification-Based Truth Maintenance

 A Justification-based truth maintenance system (JTMS) is a simple TMS where one can examine the consequences of the current set of assumptions. In JTMS labels are attacched to arcs from sentence nodes to justification nodes. This label is either "+" or "-". Then, for a justification node we can talk of its in-list, the list of its inputs with "+" label, and of its out-list, the list of its inputs with "-" label.

The meaning of sentences is not known. We can have a node representing a sentence p and one representing ~p and the two will be totally unrelated, unless relations are established between them by justifications. For example, we can write: 


		~p^p Contradiction Node
		  o
		  |
		  x		   'x' denotes a justification node
		/   \		   'o' denotes a sentence node
	      +/     \+
	      o       o
	      p      ~p
which says that if both p and ~p are IN we have a contradiction.

The association of IN or OUT labels with the nodes in a dependency network defines an in-out-labeling function. This function is consistent if:

Here are examples of JTMS operations (see Forbus&deKleer):

Here is a simple dependency network: 

	     contradiction
		   |
		   x
		   |
		 g o     o h
		   |     | 
		   x     x 
		  / \   / \
		 /   \ /   \
	        o     o     o
		A     C	    E

This network is created:
	(setq *jtms* (create-jtms "Forbus-deKleer example on page 181"))
The nodes A, C, E are created and enabled:
	(setq assumption-a (tms-create-node *jtms* "A" :assumptionp t)
	      assumption-c (tms-create-node *jtms* "C" :assumptionp t)
	      assumption-e (tms-create-node *jtms* "E" :assumptionp t))
	(enable-assumption assumption-a)
	(enable-assumption assumption-c)
	(enable-assumption assumption-e)
The node h is created and justified:
	(setq node-h (tms-create-node *jtms* "h"))
	(justify-node "R1" node-h (list assumption-c assumption-a))
				;; R1 is the informant for this 
			        ;; justification
The node g is created, justified, and established as a contradiction:
	(setq node-g (tms-create-node *jtms* "g"))
	(justify-node "R2" node-g (list assumption-a assumption-c))
	(setq contradiction (tms-create-node *jtms* 'contra :contradictoryp t))
	(justify-node "R3" contradiction (list node-g))

This last command will recognise that a contradiction exists and will
invoke a contradiction handler that should state that the node 
"contradiction" is a contradiction and that some of the assumptions 
in {A, C} should be retracted.
Here should be a larger dependency network as used in a JTMS.

Algorithms are available to propage changes in assumptions, either asserting a sentence, or retracting it. Further, algorithms are available to determine the maximally consistent sets of assumptions supporting a given sentence.

Assumption-Based Truth Maintenance

In a JTMS, we change assumptions by relabeling the nodes of a dependency network. Any time we switch among alternative sets of assumptions, we re-label the net. This may lead to considerable work.
Another possibility is to maintain information at each node within a single dependency network for all the alternative sets of assumptions that we may hold, also called worlds or environments. That is, we can use as label of a node the set consisting of all the environments that justify this node. This is the path taken in Assumption-Based Truth Maintenance Systems (ATMS). Since all environments are simultaneously available, it is not necessary to enable or retract sentences, and thus re-label the network. It is only necessary to switch from one environment to another.

The problem of the ATMS approach is that if we are given n assumptions, there are 2**n possible selections of all these assumptions, that is 2**n environments. This, except in trivial cases, is more than we can work with.

Two observations simplify this problem:

We define the context of a set A of assumptions to be the set consisting of all the nodes that hold in A, i.e. that have a justification based on A.

Here are examples of ATMS operations (see Forbus&deKleer, pg440):

create-atms (title node-string enqueue-procedure)
creates a dependency network with the same parameters as create-jtms, except that now we do not have a contradiction-handler, since the relevant information is recorded by the label.
true-node? (node)
recognises if node is a premise
why-node(node)
returns the label of node
atms-assumptions(an-atms)
returns a list of all the assumptions enabled for this atms
interpretations(atms choice-sets defaults)
returns all the environments that are consistent with defaults and include at least an element from choice-sets.
tms-create-node and justify-node are for ATMS as defined for JTMS.

Here is the same example considered for JTMS: 


    (stq *atms* (create-atms "Example from Forbus-deKleer pg.442")
    (setq assumption-a (tms-create-node *atms* "A" :assumptionp t)
	  assumption-c (tms-create-node *atms* "C" :assumptionp t)
	  assumption-e (tms-create-node *atms* "E" :assumptionp t))
    (setq node-h (tms-create-node *atms* "h"))
    (justify-node "R1" node-h (list assumption-c assumption-e))

Now the query (why-node node-h) returns the label (h {{C,E}}). Continuing:

    (setq node-g (tms-create-node *atms* "g"))
    (justify-node "R2" node-g (list assumption-a assumption-c))
    (setq contradiction (tms-create-node *atms* 
				'contradiction :contradictionp t))
    (justify-node "R3" contradiction (list node-g))

After this last statement there is no call-back from ATMS to IE. Yet
we can determine the maximally consistent sets of assumptions that are
compatible with what we know by calling:

    (mapc 'print-env 
	 (interpretations *atms* nil (atms-assumptions *atms*)))

with result:

	{A,E}
	{C,E}

Conclusions

 Truth Maintenance Systems are significant as a mechanism for implementing dependency directed backtracking during search.

Software is available on JTMS and ATMS in Forbus.

References

Appendix: The ABC example

An example by Quine and Ullian, as reported by Rich&Knight, shows typical circumstances under which people operate. We would like a problem solving system to be able to reason about cases such as this. 

   We know that:

	Abbott, Babbitt, Cabot are suspects in a murder.

	Abbott has an alibi, the registration at a good hotel in
	Albany at the time of the crime

	Babbitt has an alibi, his brother-in-law says they were
	together at the time of the crime

	Cabot says he was at a Catskills ski resort, but with no
	witnesses.

   Our other premises (i.e. assumed unconditionally) are:

	The hotel in Albany is reliable

	Babbitt's bother-in-law is reliable

   We have as current assumptions:

	(1) Abbott did not commit crime

	(2) Babbitt did not commit crime

	(3) Abbott, Babbitt, or Cabot committed the crime.

   We then find a newsreel showing Cabot at the ski resort:

	(4) Cabott did not commit the crime.

   Thus:

	(1) & (2) & (3) & (4) are contradictory beliefs

ingargiola@cis.temple.edu