A Glimpse of Truth Maintenance

A GLIMPSE OF TRUTH MAINTENANCE*·**

Jon Doyle Artificial Intelligence Laboratory Massachusetts Institute of Technology 5i!i Technology Square Cambridge, Massachusetts 02139

To choose the1r actions, reasoning programs must be able to draw conclusions from limited information and subsequently rcv1se their beliefs when discoveries invalidate previous assumptions. In the Trutla Mainttnana SyJtrm (TMS) I introduce a new notion of "reason for belief" which permits the mechanization of these abilities as a problem solver subsystem. The TMS records and maintains the reasons for program beliefs. These recorded reasons are useful in constructing explanations of program beliefs and act1ons. and in guiding the course of action of a problem solver. This paper outlines some or the structure and applications of the TMS.

I. INTRODUCTION

One amportant problem faced by reasoning programs is the nerd to make decisions based on limited information. This problem arises both in programs anteracting with an external envaronment and an contemplatave programs searching a data base for an answer to some question. There are two consequences of this need to predact; the program must have some way to rna ke dec as ions based on limited an formation, and the program mmt have some way to revise its beliefs if these decasaons are found to be in error. The first of these aballties is prov1ded by ut11izmg epistemic clamfications of pmsabiE' program bE'IIE'fs so that conclusions may be drawn from the lack of belief as well as from other beliefs. The second ability IS in general a very complex problem for which no complete solutions are known. (See [3,7,8) for survE'ys of the probiE'm.) However, the simpler problem of revasang behefs based on limited information is solvable by recordmg the reasons for each program behef. These records can be USE'd to fmd the SE't of extant beliefs by determining which beliefs have vahd reasons. These recorded reasons also are useful in resolvmg connacts that arise when limited knowledge gives rise to incompatable conclusaons. This paper desmbes a mechanazataon of these abilities, embodied in a general-purpose probiE'm solver subsystem called the Trutlr Mainttnana SyJtorl (TMS). The TMS is based on a new analysas of what constatute "reasons" for beliefs and "assumpcJ" behefs. In th1s analym, all beliefs are derived from the exastence of vahd reasons for them, and aswmptaons arc statements whach are believed because some othE'r statemE'nts are not beheved.

'-' Th1s research was conducted at the Artafacial Intelligence Laboratory of the Massachusetts Institute of Technology. Support for the Laboratory's arttfaml intelligence research is provaded an part by the Advanced Research Projects Agency of the Deputment of Defense under Office of Naval Research contract number NOOOii·75·C·06i3, and in part by NSF gaant MCS77·0i828.

.,.~ My new paper [2) presents the foundations, mechanisms, and apphcataons of the TMS in much greater depth, detail, and clanty than is passable here. That paper also mentions the many related works by others too numerous to cite in this short a paper.

The TMS records and maantams "proofs" of program beliefs. It manapulates two data structures; nodtJ , whach represent behefs. and juJtijicationJ, which rrpresent reasons for behefs. The fundamental actaons the TMS can be called upon to perform are the creataon of a new node. to wh1ch the problem ~olvmg program can attach the statement of a belief. and thE' addnaon of a new Jmtafacatton to a node, to represent assenaon of the behef assocaated with the node by some rule or procedll!e 111 the problem solver. The addltaon of new JIIStlltcataom may anvoke the automatic procedure of trutlt mcliniC111111<'r to make any IE'Vtsaons necl.'s~ary in the set of behds. The TMS revases bl.'liefs by usang the rtcordtd JUStifacataons to compute non-circular proofs of behefs from basac hypothesi's. Thesr proofs dastanguash one or more Jmttflotiom :lS the wcllfC'undcct wpt>C'rt for l':lCh btheved node. and are used during truth maantenance to determane the set of brhefs to update by fandang those nodes whose well-founded support depends on changed beliefs. These. proofs allow another process, dependency-directed backtracking. to resolve conflicts by tracing the well-founded supports of conflictmg beliefs to remove one of the assumptions causing the conflict and to make a record used tO prevents Similar future connicts.

Minsky [6) cntlcized traditional logics for their monotonicity, their lack of any ability to control mferences by the addition of new axioms. With this in mmd the TMS employs a specia I type of justification, called a non-monotonic justification, to draw conclusions based on limited or incomplete knowledge. This type of JUStification allows belief m a node to be based not only on other beliefs, as occurs in the standard forms of deduction and reasoning, but also on lack of belief 111 certain nodes. For example, a node N-1 rcprescntmg a statement P m1ght be justified on the basis of a lack of bl'hef in a node N-2 representing the belief "'P. (Distinct nodes are used to represent P and "'P.) In this case, the T M S would have N-1 believed as long as N-2 was not believed. and we would call N-1 an assumption. (More generally, by assumption we mean any node whose well-founded support is a non-monotonic justification.)

As a sma II example, suppose an office scheduling program is considenng holding a meeting M on Wednesday. To do th1s. the program assumes that the meeting is on Wednesday. The data base of the program mcludes a rule which draws the conclusiOn that due to regular commilments, any meeting on Wednesday must occur at 1:00 PM. However, the fragment of the schedule for the week constructed so far has somethmg else scheduled for that time already, and so another rule m the data base concludes that the day for the meetmg cannot be Wednesday. These beliefs might be notated as follows:

As seen in the above notatiOn for justifications, each justification consists of two ltsts. The meaning of the notation 1s that the statement depends on each of the nodes an the farst list bemg believed, and on each of the nodes in the second list not being believed. Since there is no known JUStification for N-2. it 1s not believed. The JUStification for N-1 spec1f1es that it depends on the lack of belief in N-2, and so N-1 IS believed. The JUStifiCation for N-3 shows that it is believed due to rule R- 37 acttng on N-1 . When the assumption N-1 is rejected by some rule,

N-2

DAY i Ml " WEONESOA Y

ISL IR-9 N-7 N-81 (II

where N-7 and N-8 represent the day and time of some other engagement, the TMS will revise the beliefs so that N-1 and N-3 are not believed.

2. REPRESENTATION OF KNOWLEDGE ABOUT BELIEF

A node may have several justifications, each of which represents a different reason for belief in the node. The node is believed if at least one of these justifications is valid. The conditions for validity of justifications are described below. We say that a node which has a vahd JUStification is in, and that a node without a valid JUStification is out. The distinction betWE'E'n in and out is not that of true and Jalst. The former classification denotes conditions of knowledge about reasons for belief; the exiStence or non-existence of vahd reasons. Trru and Jalu, on the other hand, classify statE'ments according to truth value independent of any reasons for belief. In this way, there can be four states of knowledge about a proposition P, corresponding to the node representing P being in or out and the node representing .,p being in or out.

There are two basic forms of justifications. These are inspired by the typical forms of arguments in natural deduction mference systems. A sample proof in such a system m1ght be as follows:

Each step of the proof has a line number, a statement, a justification. and the set of hne numbers the statement depends on. Prem1ses and hypotheses depend on themselves, and other lines depend on the set of premises and hypotheses derived from the1r JUStifications. The above proof proves A:::>C from the premiSE'S A:>B and B:::>C by hypothesizmg A and concluding C. The assumption A is then discharged to prov1de the proof of A:::>C . There are two effects that JUStifiCations can have on the set of dependencies in natural deductiOn systems; either the justifications can sum the dependencies of the referenced lines (as in line i). or they can subtract the dependencies of some lanes from those of other hnes (as 111 hne 6). The two types of justifications used in a T M S account for these effects on dependencies. A mJ>part-list ( S L) justification says that the JUStified node depends on a set of other nodes. and thus 111 effect sums the dependencies of the referenced nodes. A conditional-proof

(C P) justification says that the node it justifies depends on the validity of a certain hypothetical argument, and as in the example above, subtracts the dependencies of some nodes (the hypotheses of the hypothetical argument) from the dependencies of others (the conclusion of the hypothetical argument). These two types of justifications can be used to construct a variety of forms of dependency relationships. For example, we might rewrite the example in terms of TMS justifications as follows (here ignoring the difference between premises and hypotheses, and ignoring the inference rule MP):

The support· list justification is of the form

ISL <in I i st> <OUt I i st>l.

A SL·justification is valid if each node in its inlist is in, and each node in its orttlist is out. A SL·justification can be used to r<'presC'nt several types of deductions. When both the inhst and outlist are empty. we say the justification forms a prrmiu justification. A premise justification is always valid, and so the node it justifies will always be believed. Normal deductions are represented by support-list JUStifications with empty outlists. These r<'present monotonic deductions of the JUStifred node from belief in the nodes of the inlist. Assumptions are nodes whose well-founded support is a support-list JUStification with a nonempty outlist. These justifications can be interpreted by viewing the nodes of the inlist as comprising the reasons for making the assumption; the nodes of the olltlrst represent the specific incompletenesses of knowledge authorizing the assumption.

The conditional-proof justrfication takes the form

ICP <consequent> <inhypotheses> <Outhypotheses>l.

A node JUStified by such a justification represents an implication, whose support IS derived by a conditional proof of the consequent node from the hypothesis nodes. A justification of this form is valid if the consequent node is tn whenever (a) each node of the in hypotheses is tn and (b)each node of the outhypotheses is out. Except in a few esoteric uses, the set of ollthypothesrs is empty. Standard conditional proofs in natural deduction systems specify a single set of hypotheses, which correspond to our tnhypotheses. The truth maintenance system requires that the set of hypotheses be divided rnto two disjornt subsets, since nodes may be derived both from some nodes being In and other nodes being out.

3. DEFAULT ASSUMPTIONS

One very common technique used in problem solving systems is to specify a default choice for the value of some quantity. (See, for example, [8).) This choice is made with the intent of overriding it if either a good reason is found for using some other value, or if making the default choice leads to an inconsistency. The assumption of the day of the week for a meeting in the first example above is such a default assumption.

In the case of a binary choice, a default assumption can be represented by believing a node if the node representing its negation is out. When the default is chosen from a set of alternatives, the following generahzation of the binary case is used. Let IF 1 · ... , F nl be the set of the nodes which represent each o( the pouible values of the choice. Let G be a node which represents the reason for making the default assumption. Then Fi may be made the default choice by provrding it with the justificoltion

If no information about the choice exists, there will be no reasons for believing any of the alternatives except Fi. Thus Fi will be in and each of the other alternatives will be out. If some other alternative receives a valid justificat ion from other sources, that alternative will become in. This will invalidate the support of Fi, and Fi will become out. If a contradrction is derived from Fi , the dependency-di rected backtracking mechanism will recognize that F 1 is an assumption by means of its dependence on the other alternatives being out. (See the section on dependency-directed backtracking for an explanation of this.) The remit of backtracking may be to JUStify one of the other alternatives, say Fj' causmg Fi to go out. The justification for F j will be of the form

where the remainders are the Fk's remaining after Fi and Fj are taken away. In effect, backtracking will cause the removal of the default choice with the set of alternatives, and wall set up a new default assumption structure from the remaining alternatives. As a concrete example, our scheduling program might default a meeting day as follows:

N-2

DAY IMI · WEDNESDAY

ISL II IN-1 N-31 I

N-3 DAYIMI ·FRIDAY

In this example, Wednesday is assumed to be the day of the meetmg M, with Monday and Friday being the alternatives. Wednesday will be the default cho1ce until a valid reason is supplied for either Monday or Friday.

If the complete set of alternatives from which the default assumption 1s to be chosen cannot be known in advance but must be dmovered piecemeal, a slightly different structure is necessary. This ability to extend the set of alternatives is neccssa ry. for example, when the default is a number, due to the la1 ge set of poss1ble alternatives. For cases like this the followmg structure may be used instead. Retaining the above notat ion, let ""F i be a new node which will represent the negation of Fi' We will arrange for F; to be believed if ""F i cannot be proven, and will set up JUStifications so that if Fj 1s dmmct from Fi , Fj w1ll imply ""Fi. This is done by givmg Fi the JUStificatiOn

and by giving ""Fi a justification of the form

for each alternative Fj distinct from Fi. As before, Fi will bE' a ssumE>d if no reasons for using any other alternative E'XISt. Furthermore. new alternatives can be added to the set s1mply by g1ving ""Fi a new justification corresponding to the IH'W altl'rnatlve. This structure for default assumptions will behave as did the f1xed structure in the case of an unsr.lecred alternatiVE' receiving independent support. B<~cktrackme;. however, has a d1fferent effect. If a contradiction IS denved from the default assumption supported by the extensible structure, ""Fi w1ll be justified so as rn make Fi become out. If th1s happens, no alternative will hr srlr.ctf'd to take the place of the default assumption. The rxtem1ble structure re"juires an external mechanism to comtruct a new df"fault assumption whenever the current drfault 1s ruled out. For example, a census program might make aswmpt1ons <~bout the number of children in a family ilS follows:

Wnh th1s system· of JUStifiCations, N-1 would be believed because no different number of children is known. If it turns out th<tt the family h<ts, for example, 5 children a new statement would have to be made, along with a new JUStification of N-2 in terms of this new statement.

4. DEPENDENCY-DIRECTED BACKTRACKING

Making assumptions admits the possibility of making errors. When a contradiction or other inconsistent state of the data base occurs, the TMS employs a process called dependency-directed backtracking to find and remove incorrect assumptions so as to restore consistency. There are several steps involved in dependency·d1rected backtracking, but first the inconsistency must somehow be signalled to the TMS. as there is no built-in notion of inconsistency. This signalling consists of informing the TMS that a node represents an inconsistency. With this knowledge, the TMS w1ll try to restore consistency whenever the node comes in by reJecting enough assumptions to force the node out. Any node may be marked for such treatment. A node so marked is called a contradiction.

The steps of dependency-directed backtracking are as follows. F1nt, the well-founded support of the contradiction node Is traced back wards to find the set of assumptions (nodes with a non-monotonic justification as their well-founded support) underlying the contradiction. Belief tn at least one of these assumptions must be retracted to remove the contradiction. This is done by creating a new justiftcation for one of the out nodes underlying one of the assumptions. Since the backtracker may be mistaken in its assignment of blame to that assumption, the justification used to retract the assumpt1on must indicate the alternatives that wrre available but not uulized by the backtracker. Thus the new justtficauon includes (a) the reason why the contradiction occurred and (b) the other assumptions involved. Thus the second step of the backtracking process is to construct a node recording the reason why the contradiction occurred, and the third step is to use this node and the other assumptions In justifymg an C1llt node supporting the assumption selected for removal.

In more detail, the first step of the backtracking process traces backwards through the well-founded support of the contradiction node to collect the set of "maximal" assumptions supporting the contradacllon. Not all assumptions found by tracing the well-founded support are used; instead, only those assumptions which do not support other assumptions underlymg the contradtctlon as well. That is, the well-founded support relationships induce a natural partial-ordering on nodes, where one node is said to be "lower" than a second node if the first occurs in the second's well-founded support. The maximal assumptions are then thme assumptions which <He maximal in this partial order. Only this "front line" of assumptions is used because if the rrason for revokmg a lower-level assumption involves a highrr-lrvrl assumption, then the removal of the lower-level assumptiOn would cause truth mamtenance to remove the h1gher·level assumption that it supports, so the reason for rrmoving the lower-level assumption would not hold up. This reflr.cts the fact that there may not be enough information to definitely rule out a lower-level assumption.

The srcond step summarizes the reason for the contradiction in terms of the set of selected assumptions. Let S · {A 1 · ... , An} indicate thr set of inconsistent assumptions. The backtrlcker then creates a node called a nogood, a new node s1gmfymg that S is inconmtent. Since contradiction nodes really represent the false statement, the nogood node can be taken to represent

or alternatively,

S is recorded as the nogood·sct of the nogood. This meaning for the nogood node is produced by justifying it with the. cond1t10nal proof of the contradiction node relative to the assumption nodes, that is, With the justification

In this way, the inconsistency of the set of assumptions will be remembered even after the contradiction has been resolved by the retraction of some hypothesis.

The final strp is selectmg an assumption A 1 (the "culprit") from S and justifying one of the out nodes listed in its well-foundrd supportmg justification. (If these underlying out nodes <He thought of as "denials" of the assumption, then this step is much hke reasonmg by rtductio ad absurclurn.) Let N(; be the nogood. and let the mconsistent assumptions be A 1 · ... · An. Let D 1 · ... · Dk. be the out nodes appearing in the JUStification which supports belief in the assumption A 1 . This justification for the assumption can be invalidated by justifying D 1 with the justification

This jliStlflcation is valid whenever the nogood and other assumptions are believed and the other "denials" of the culpnt are not believed. If the choice of culpnt was in error, thrn another contradiction will occur in the future involving D 1 · and by this just1f1cat1on w11l be led to suspect the remaining assumptions, as well as D 1 if there are any other out nodes listed in its justification. If, by means of other previOusly existing JUStifications, the current contradiction is still in followmg the addition of this justification, backtracking is repeated. Presumably the new invocation of the bJcktrackmg process will find that the previous culprit is no longer an assumption. Backtracking halts when the contradiction becomes out, or when no assumptions can be found underlying the contradiction.

As an example, consider a program scheduling a meeting, preferably at 10 AM in either room 813 or 801. This might be represented as:

N-1 TltlEIMI ·1000

N-2 T I ME 1M I " 1 000

N-3 ROOM IMI · 813

N-4 ROOM IMI · 801

With thrse JUStifications, N-1 and N-3 are In, and the other two nodes are out. If some previously scheduled meeting exists, It might cause this combination of time and room for the meetmg to be ruled out by means of a contradiction.

ISL IN-1 N-31 () l

The deprndrncy·dlrected backtrackmg system then traces the weiHoundrd support of the contradiction to find that it depends on two assumptions, N-1 and N-3, both of which are maximal.

A nogood node is created wh1ch means, in accordance with form (I) above,

and this nogood is givt·n a JUStificatiOn correspondmg to form (~) above. The assumption N-3 1s selected arbitrarily as the culprit. and is rejected by providing Its only out supportmg nodr, N-4, with a JUStlflcauon of the form (3) above. Followmg this, N- 1. N-4, and N-6 are in, and N-2. N-3, and N-5 are out. N-6, the nogood node, has an always-valid CP·JUSllflcatlon smce the contradiction node N-5 drprnds directly on the two assumptions N-1 and N-3 without any additiOnal behefs mtervenmg. If some further com1derat1on determines that room 801 cannot be used after all, another contradiction node could be created to force a different cho1ce.

N-7 CONTRADICTION ISL IN-41 ll I

ISL () IN-21 l

ISL ll IN-41

N-8

N-2

NOGOOO N-1

TIMEIMI "1eee ICP N- 7 IN-11 Ill ISL IN-81 II l

Tracing backwards from N-7 through N-4, N-6, and N-1, the backtracker fmds that the contradiction depends on only one assumption, N-1. The nogood node N-8 is created and justified with a CP-justification which in effect is equivalent to the SL-justification

ISL IN-61 I II,

since the nogood N-6 contributes to the contradiction but does not Itself depend on the assumption N-1. The revocation of the assumption N-1 removes N-5, the previous objection to the choice of room, so at the close of this bit of decisiOn making N- 2, N-3, N-6, and N-8 are in, and N-1, N-4, N-5, and N-7 are out.

There are a number of variations on this particular scheme for dependency·d1rected backtracking. All of these variations are constderable improvements over the chronological backtrackmg systems used in claSSical systems like MICRO-PLANNER and many early theorem provers. The improvements stem from the non-chronological nature of dependency-cltrected backtracking, in which the support relationships rather than the temporal orderings determine the choices responsible for an error. Another improvement is that the cause of the contradiction is summarized via a nogood node. This summarization keeps the system from making the same mistake in the future. Stallman and Sussman [10] mdicate that these two improvements lead to sizable gains in efficiency.

5. DISCUSSION

The TMS solves part of the problems of belief revision and limited mformation by mtroducmg new conceptions of justified behef, JUStification, and assumption. It lends itself to several other uses as well as belief revision and making assumpt1ons: for example, providing explanations of program beliefs and actions (see [2)). and controlling the problem solvt>r's actions (set> [1,2,10)). London [4) explores in detail the usl' of dependency networks in updating a problt>m solver world model · in the face of actions. For the mathematically oriented, Drew McDermott and I try to analyze the logic and semantics underlying the TMS in [5). Non-monotonic logic, as we ca ll it , has several novel properties.

ACKNOWLEDGEMENTS

I thank Gerald Jay Sussman, R1cha rd M. Stallman, Guy L. Steele J r. , Johan de Kleer, Drew McDermott, David McAIIe~te r , Scott Fahlman, Howard Shrobe, Charles Rich, Marilyn Matz, Beth Levin, Jim Stansfield, Mitchell Marcus, and Richard Brown for ideas, comments and advice, and the Fannie and John Ht>rtz Foundation for supporting my research with a graduate fellowship.