The Ins and Outs of Reason Maintenance

ABSTRACT

To progress 8ignifica.nt.ly beyond current reason maintenance systems, we must formulate their structure and intended behavior precisely "nough t.o :malyzc computational complexities and tradcotls indepen­ dently of the curren t set, of limitcil implcmeotation propom1.ls. This paper summarizes one ::such formula.i.ion, and indicates somt~ unsolved practical problems for investigation in future reason maintenance sys­ tems.

1. Tleason maintenance syst~ms (a less deceptive n:>me than the original "truth maintenance systems") have been studied by a variety of a11thors and have gained currency if'. artificial intc]Jigence in spite of rather unwieldy descriptions in terms of complex procedures. (Sec [DOYLE 1979], [STALLMAN AND SUSSMAN 1977], [LONDON 1978), [MCALLESTER 1980), [CHARNIAK, !lTESBECK, AND MCDERMOTT 1980), [THOMPSON 1979), [G AIWENFORS 1980), [STEELE 1980), [DE KLEEit AND DOYLE 1982), [MCDERMOTT 1982), [GOODWIN 1982), and [MARTINS 1983] .) There is little hope for improving on existing RMS implementations without clearer statements of their intended be­ haviors and better analyses of their performance (see [MARTINS 1983]). These goals require mathematical formulations that clearly capture our intuitions, formulations that enable calculation of complexity-theoretic tradcofTs to guide and justify choices <;>f implementation. [DOYLE 1982] develops exact. theo ries and initial analyses of several issues arising in reason maintenance systems and in "non-monotonic logic." This paper summarizes portions of those theories and some of the questions they raise.
2. §2. Reason maintenance systems revise database states using records of inferences or computations, records called reasons or justifications, to trace the consequences of ini t ial changes. 13y keeping track: of what. information has been computed from what, such a system can reconstruct the information "derivable" from given information. Al­ though it is often convenient to think of such bits of information as beliefs and such derivations as arguments, the notion is much more general, applicable instead to all sorts of mental structures. For con­ t'ieteness, we focus on RMS, the particular reason maintenance system

This research was supported by the Defense Advanced Research Pro­ jects Agency (DOD), ARPA Order No. 3597, monitored by the Air Force Avionics Laboratory under Contract F33615-81-K-1539. The views and conclusions contained in this document are those of the author, and should not be interpreted as representing the official policies either expressed or implied, of the Defense Advanced Research Projects Agency or the Government of the United Stat.es of America.

THE INS AND OUTS OF REASON MAINTENANCE

Jon Doyle

Computer Science Department Carnegie-Mellon University Pittsburgh, Pennsylvania \52\3 U.S.A.

developed by the author [DOYL" 1979]. The following treatment does not require int.imate familiarity with any rellson maintenance system, although in the interest of brevity we omit motivating discu,sion and examples, so pa5Siug acquaintance with the basic idea stated above is valuable. Here we only-mention that, contrary to the impression held by 8ome, RMS does not maintain consistency of beliefs in any impor­ tant sense. RMS ensures that the set of "beliefs" held arc acceptable with respect \,o the justifications held, or in other, looser ter(11inol­ ogy, that the assumptions rn:tdc by the system are consistent with the justifications guiding their adoption. Logit:al notions of consistency play no role here, as the following treatment illustrates. The mistaken impression may stern from th~ contrasting importance of logical con­ sistency in "non-monotonic lo~;ic" [McDERMOTT AND DOYLE 1980] . (See [DOYLE 1982] for further discussion.)

• §3. States of llMS contain a variety of elements or components. We let D denote the domain of all possible elements of states, so that states of RMS are sets S ~ D. Not every subset of D is "admissible" as a state of llMS. We define which sets are so in a moment.

Let J./ be a finite set of elements called nodes. These arc the fundamental components of states of RMS. Nodes arc usually used to represent (within RMS) the databaec elements (beliefs, desires, rules, procedures, etc.) of significance to the external system using RMS, but we ignore those external meanings here since they have no bearing on the operation of RMS. Each set }/ generates a state-domain D(JJ) as follows. We define

(P' means power set.) The clements of SL(JJ) are called SL-juatifications (for "support list"), and are written A II R If- c for A, B ~ )J and c E JJ. The clements of CP(JJ) are called CP-justifications (for "conditional proof"), and are written (A II B If- c) If- d for A, B ~ )J and c, dE JJ. SL-justifications will be interpreted as rules for ma.king "non-monotonic" inferences, and CP-justifications as arguments based on "conditional-proofs" of nodes. The formal definitions of these terms follow. Note that if )J ~ JJ', then D(JJ) ~ D(JJ'). In fact, all of our definitions will be conservative in the sense that additions to the set of nodes do not change the meaning of previous conclusions or representations in important ways. Henceforth we hold the set of nodes constant and ignore the dependence of the domain on the set of nodes writing simply D instead of D(JJ). '

§4. Each slate component is int.~rprcled as a rcstridion on the stat.es in which it may admissibly occur. l·'ormally, we define an interpretation funr.tion I : D _, P P D, where if d E D, then I(d) ~ P D is the set :>f potential states sanctioned by d. The set j of admissible slates of RMS is defined to coulain just those sets of c01nponcnts which are com plclely self-satisfying, specifically,

We define interpretations for nodes, SL-justifications, and CP-justifica­ tions as follows.

There arc two sorts of nodes: ordinary uodcs, and contradic­ tion nodes. The user of RMS stipulal.es the sort of c;;ch node explicitly by labelling contradiction nod~s as ""ch. Ordinary nodes have no spe­ cial meaning to RMS, except that they arc distinct from other nodes. Contradiction no<ks, in contrast, clo have special meaning: RMS avoids including them in states. We name th~sc t.wo sets of nodes ).1 T and J.I .L respectively, so that J.l = J.IT U J.I ·L. If n E J.I T, then I(n) = P D, the "trivial" specification on states which rules out no potential states. lf n E J.l l. , then I(n) = 0, the "contradictory" specification which ar.cepts no states.

(Be= D - JJ.) That is, e specifir.s that if S ccntains every clement of A and contains no. ele111ent of B, then S mus t abo contain c in order to be admissible. In RMS parlance, we s:1y that if every element of A is in and every clement of 1J is out, then c must be in as well.

If e =(A II B If- c) If-dis a CP-justification, then intuitively, the CP-justification is satisfied if dis inS whenever cis in all admissible >Latcs as close as possible to S that contain all elements of A and none of B. We express this formally by defining

where

and

For this definition, we measure closeness of a state to Sin terms of th< set of clements by which the two differ, namely the symmetric difTerenc< S /::;; S' = (S- S') U (S'- S). Other notions of closeness may be usee instead if desired, but, we cannot pursue them here.

§5. Given a set of nodes and justifications S ~ D, the action of RMS is to derive an admissible state H containing S by adding additional nodes to S. Since f) is admissible, it satisfies all the specilications represented by t.hc clements of S. However, we do not acc.,pt every admissible su­ perset of S as a reasonable solution to the requirements posed by S, since some of these supersets may introduce nodes and justifications completely unrelated to those ment ioned in S. (Analogously, in logic the set of theorems of a set of axioms is the cleductive closure of the axioms. The theorems form a deductively dosed set, but there may be larger deductively closed sets containing the axiom,.. whose extra elements have nothing to do wit.h the axioms.) To avoid unwarranted addit.ions to the initial set S, we define the admis.,iblc extensions of 8, written A E'xts(S), to be the aclmissible sets /<.' :::2 S finitely grounded with respect to S, where E is llnilcly grounded with respect to S if and only if for every e E E there is a finite s~qucncc (!Jo, . . . , !Jn) of clements of E such that e = 9n and for each i S n, either

• (I) g; E S, or
• there is some j < i such that

(a) !J; =A II JJ If-!];,

(b) for each a E A, a.= !Jk for some k < j, and

(c) b rf:. E for each bE JJ, or

1. there is some j < i such that

(b) c E F:' for each E' E 71(E, A, B).

In other words, E is finitely grounded with respect to S if every clement of E has a non-circular argument from 8 in terms of valid jus tifications in E. In general a set S ~ D may have any m·unber (0 or more) of ad­ missible extensions. Note that while the antecedents of SL-justifications must occur in such arguments, valid CP-justifications arc simply looked on as "oracles" about other admissible states. H.MS actually employs an approxirilation scheme instead of oracles, but it is too complicated to present here.

§6. In [DOYU; I 982] we develop at length the theory of this for­ mulation of nodes and SL-justificat.ions, leav ing a.!ide CP-justifications. That treatment is too long to reproduce here, but we can sketch a few of the principal results. First, one can stratify by construction ev.ory admissible extension into a series of levels A;(S, E) corresponding to the the lengths of the shortest arguments for clements of B from S, with Ao(S, E) = S and A..,(S, E) = U::o A;(S, E). The first main result turns the same construction around to show that any set constructed in this way must be an admissible extension. This fact is important in proof of correctness of RMS algorithms.

A corollary of this is that admissible extensions are set-inclusion mini­ mal.

(6.2) COROLLARY (MINIMALITY). If R, F:' E AExts(S) and E ~ E', then E = E'.

A related result is that distinct admissible extens ions must share some SL-justi!ication that "upports conclusions in one extension but not in the other, and so represent incompatible intcrpret.ations of the common justifications.

(6.3) THEOREM (STRONG VAI.IDITY-0PTIMALITY). If E,E' E AExts(S) and E of E', then there ;, some t E En E' such that e = A II fJ If- c and either A ~ F: ~ Be but not A ~ E' ~ Be, or A ~ E' ~ ne but not A ~ E ~ nc.

In the longer treatment we also show that E E AExts(S) can be checked in time O(IDI 3 ). I do not know if one can construct admissible extcn­ ·ions in polynomial time. Admissibility of states can also be checked in polynomial time. I do not yet know how bad the complexities becom£ when CP-justifications are considered.

• §7. RMS not only construds admissible cxt<'nRions of scl,s of nodes :\lid justificati:ms, it also upd:ttcs t.he state whenever reasons arc added to or dclded from a '·kernel" s<:t. After IUv!S leaves t.he uatabasc in state 8, t.he external program using RMS c:ornputes a new kernel set iJ(S) of jus tifications from S. We write ~(S') lo mean the set of admis.1ible tranBition.· from (o· successo1·s or) S, the intent being that RMS revise the state to be an admissible extension of the new kernel. If we allow any revision, then ~(S) = ARxls(8(S)), so the complexity questions rnentioneu carl;cr about co11structing lulmissible extensions have consiuerablc practical importlwce. A more interesting possibility is to require ~ to be con·ervative, that is, to allow only tran~itions to those states in Al~:cto(D(S)) whidt arc as close as possible to S. Here we agai11 dra.w on the symmetric difTerence comparison of states introuuced ea~licr, and define the conservative transition table ~" by ~"(S') = v(S,ABxts(D(S))). It would be very valuable to have conservative versions of RMS, since then successor states would look a:; much like their prcdece;sors as possible. Unfortunately, the efficient mechani·abili ty of conservative transitions is"" open question. 13ecause of this, RMS was implemented to "apptoxi111atc" conservative revisions in the sense of probabilistic algorithms. These "approximations" are always a<lmiso!ble extensions, · but sometimes may fail to be minimal transitions due to the limited information used in the "local" choices made by the revision algorithm.

§8. If ~(S) = (2) because the external program include" in a(S) a con­ tradiction node or a justification to support a cont.radicLion node, then Rl'\'IS must perform "backtracking" to find a new stale not containing any contradiction node. (One limitation of RMS corrected in some of it· relatives is abnormal failure if ~(S) = 0 without S containing any contradictions.) RMS backtracks by adding some new justifications A to the kernel D(S) in hopes that B(S) U A will have admissible exten­ sions. ltMS chooses new justifications to add so as to find a previously bypassed admissible transition as close as possible to the current state. Specifically, if (S;)i=~o is the sequence of previous states, we can treat the intended behavior of RMS a:; that of retreating to some state in v(S, U~ 0 (~(S;) - {S;+I}) ). However, I cannot exactly characterize the "ne:uness" relation actually realized by RMS as v, because RMS only uses a heuristic choice based on the structure of the arguments which support contradiction nodes. Can RMS be improved to employ the same conservation principles in both backtracking and ordinary state transitions? It may be that M.CALLESTF~R'S and GOODWIN'S improvements to RMS do so, but I have not yet been able to perform the necessary analysis. Sec [DOYLE 1982] for a discussion of a variety of possible backtracking schemes from this point of view.

§0. The preceding presents an mcact specification for many aspects of RMS, and specifications of ideal behavior for other aspects, such as interpretation of CP-justifications, where RMS employs half-measures. Unfortunately, unanswered questions of computational feasibility and RMS's informal historical development prevent the actual program from living up to the full set of ideal specifications. With these ex­ act specifications, can we now do better? And if the particular charac­ terizations of conservative transitions and CP-justification satisfiability arc provably _intractable (or more likely, provably Nl'-hard), arc there efficiently computable . relations that approximate these well in some (perhaps probabilistic) sense?