Network Truth Maintenance for Deduction and Modelling

1. In& Deyelooment Qf Truth-Maintenance

1.1 Introduction

The problem of modelling the consequences of an action has been central to the development of automated symbolic problem solving. Selection of proper strategies for accomplishing goals may be done only when the machine has an accurate model of the state of the world at each decision point (or else has a model of its own uncertainty). Earl! systems required a programmer to associate w th each action des­ cript ion a complete representation of the changes that should be made to the world model when the execution of the action was simulated. In hi ghly coupled problem domains where single actions may alter large numbers of states * this requirement can lead to a difficult pro­ gramming problem. If an unrestricted hierarchy of definitions is allowed, the consequences of act ions may become highly context dependent and t he problem of simply enumerating the affected states can easily become intractable.

In integrated problem-solving systems, in which planning and world-modelling are combined with automatic inference from logical relations it becomes highly desirable for the modelling'com­ ponen t to employ the same logical relationships used by the inference process. Thus, if some planned action changes a state that had been inferred from previous states, then its sup­ port i ng antecedents must also be changed ("re­ futed support"). Similarly if the changed state had previously been use~ as the justifi-

* The following definitions apply to this discussion: A statement is represented as an fxore! ston (normally a Predicate Calculus ormu a . Expressions are stored in an indexed (associative) database as ~. A~ is the t ruth state (represe~by a ~ (TV), such as true 1 false, etc.) of a no e--ror its associated sta~ement). fXiom~ or~ are statement s of known truth va ue w ose state may not be changed . Statement connecttres include the normal truth-functional connec ves (AND, OR, etc. ) plus connectives for representing causali ty .

** This paper presents the results of one phase of research carried out at the Jet Pro­ pulsion Laboratory, California Institute of Technology, under Contract No. NAS 7-100, sponsored by the National Aeronautics and Space Administ ration.

cation for another state, then the dependent state may no longer be justifiably believed ("lost support"). Also, the new state may provide a justification for logically dependent states ("discovered support"). These concepts led to the notion of logical dependency as a means of maintaining the justifications of derived states and of a process of "Truth Maintenance" (TM) as a means of determining the state of belief or disbelief in expressions as a consequence of changes to the database.

1.2 Previous related~

The most complete recent systems employing TM techniques are those of Doyle [2) and London l5] . Although these systems are based on similar theoretical grounds, they differ widely in implementation and application. Doyle's system uses dependencies to determine the consequences of assumptions , to identify incon­ sistent sets of assumptions and to control backtracking . London's system is designed for modelling the consequences of proposed action sequences. Both of these systems allow knowledge to be expressed in localized "chunks" with the coupling to other chunks accomplished by the dependency network. Both systems depend upon a separate inference module to compute the initial justifications for states, which are then used by the TM process. In both cases, the dependencies must be explicitly declared by the inference process in clause form, i.e., as (the conjunction of) a list of the antecedents of the derived state.

A thorough background discussion on the use of logical dependencies may be found in the refer­ enced works; this discussion is restricted to certain generalizations of the earlier methods and with the solutions to certain difficulties encountered in the use of dependencies for world-modelling. Only examples in proposi­ tional logic will be illustrated: the methods have been extended to first-order, but are not implemented as of this writing. (This is an abridged version of the original paper, which can be obtained from the author.)

1.3 Motivation~ Features Qf ~ J£L ~

The "ERIS"+ system being developed at JPL is designed to generalize and improve the the TM and deductive processes in several respects.

+ERIS was the Greek goddess of discord.

**

The propagation of logical support, one of the primary functions of truth maintenance (discov­ ered support), is also required by deduction; as deduct1on pursues potential proofs, the dis­ covery of an actual proof should result in marking the valid line of support. In addi­ tion, by removing the restr1ction that depen­ dencles be explicitly declared in clause form, considerable structural manipulation could be avoided during TM processing. In ERIS, gener­ alized T~l procedures have been developed that are combined with the deductive process, resulting in a significant reduction in symbol/structure manipulation during deduction.

Rule-based systems often have the restriction that knowledge be expressed in clause form with inference (and therefore logical support} directed only from the antecedent to the conse­ quent of implicative rules. Since this syntax restriction can often prove burdensome, espe­ cially to non-programmers a more general rerresentation was desired, in which domain ax oms could be expressed us1ng any combination of relational connectives. The SRI "SNIFFER" system emp,loyed such a representation, but required 'extraction" rules to place the term to be proved in the consequent of an impli­ cation L3]. In ERIS, by defining TM behavior for each statement connective the need for applying rewrite rules to reformulate domain axioms as implications during deduction has been eliminated by a graph labelling procedure that determines logical support. Also, there is no need to conduct a separate search for a proof of a statement's negat1on, since the TM process may result in the discovery of a line of support for either result.

Previous work has demonstrated the advantages of dependency methods over linear (chrono­ logical) context layer schemes for the control of backtracking (see [4], [5], [2]), but context switching for purposes of hypothetical reasoning or multi-world modelling requires considerable computation using dependencies alone, as compared to typical "context-list" schemes. Although ERIS uses dependencies to control backtracking (by identifying the par­ ticular assumptions responsible for conflicts), the use of context layers is available for these other activities. Furthermore, by allowing the definition of a particular sub­ context for modelling purposes, the combined dependency/context scheme permits the same TM procedures to be used for both deduction and modelling, even though different behavior results. This method has resulted in greater accuracy in world-modelling than London's dependency-based technique, upon which it is based.

when the truth value of a statement is not known, the deductive process may have to examine all applicable axioms for a derivation. Focus of attention during the search is the key factor in determining the effectiveness of a deduction method when the number of domain axioms is large. In a manner analogous to the propagation of logical support for known truth values, focus of attention during deduction is propagated through the network of expressions using "meta" truth values that contain control information, such as the type of search (de­ duction, planning, etc.), ~r1ority, strategy advice, etc. The meta-TV sallow efficient, uniform treatment of all the propagation rules associated with statement connectives, and, by initial propagation through the domain axioms to possible antecedents of relevant nodes, they provide a way or dclimi ting the subdomain within which the forward (antecedent) reasoning of TM behavior is allowed. This restriction of forward inference is essential in unbounded domains to suppress the generation of irrele­ vant assertions. Moreover, when domain­ dependent deductive strategy information is available (as a supplement to generalized syntactical strategy rules), the control infor­ mation in the database can be explicitly accessed by modal operators that may be used in strategy advice expressions. Similar use of modal operators for control information was available in the HIT AMORD/TMS system [ 2, 1].

2. ~ ~ Qf Network l£Qlh Maintenance

2.1 1b& Definition Qf Statement Connectives

The truth-functional connectives of symbolic logic are defined by associating with the name of the connective an encoded set of rules that govern the behavior of expressions formed with the connective. The rules determine the ways in which the expression can provide logical support to the subexpressions it connects (and vice versa) and are responsible for propagating the consequences of changes in support to the affected expressions. For efficiency the rules are embedded in a procedural specialist for the connective. When a new TV is asserted for an argument of a connective expression or an entire expression, the special1st examines the TV's of the expression and its arguments . Knowledge of the truth table for a connective is embedded in its specialist and is used to find a consistent labelling of the expression and its arguments. If the new TV was assigned to the expression, then the TV's of the argu­ ments may have to be changed; if the new TV was assigned to one of the arguments, then the TV of the expression may change unless the expression is acting as an axiom, in which case the TV of some other argument may have to change. The specialists are also responsible for propagating control information during deduction or planning. Connectives used to represent knowledge of causality are defined to the system similarly, by providing an appro­ priate procedural spec1alist.

2.2 ~ li2.t..i..Qn Qf ~ "Consistency Context"

Any connective expression may behave as an axiom by having "current" support for its truth value. Truth values are context sensitive; an expression may have one truth value in a given context and a different one in another context or in an earlier "layer" of the given context . A special subcontext 1 called the "Consistency Context" (CC), def1nes the subcontext within which logical support for one truth value may not be refuted by a contradictory line of support. Normal TM guarantees that TV's of true or false are well-founded, that is, that they do not depend upon a circular justifi­ cation [2). Durin~ deduction the CC is identical with the ent1re context 1 well-founded TV's may not change, and contrad1ctions result in retracting the offending assumptions (as in [5]). During modelling however, the CC con­ tains only the current sel of axioms and those changes made SINCE the (modelled) execution of the most recent action. Lines of support within the CC may override other support, per­ mitting the network to change so that it reflects the world state after the execution of the action. Truth values in the global plan con t ext are assumed not to change unless so forced by new support. .Axioms behave as such by the fact that their TV is in the CC, so that even subexpressions may behave as axioms if thei r TV has well-founded support within the CC. For example, given the axiom (IMPLIES A (OR B C)) 1 support for the truth of A will cause the dlsjunction to behave as an axiom i.e . , if B is known to be false, then C will b~ label led true.

2.3 Operation DY£1ng World-Modelling

There are several problems associated with the use of dependencies for world-modelling relating to the requirement for refuting ali logical support for a changed state. These problems are: local uncertainty, global uncer­ tainty, and the need for adequate domain knowledge. Local uncertainty arises in cases where support derives from mulitple antece­ dents! so there is more than one possible label ing that refutes the support should the consequent be changed by an action. Suppose that C was originally proved true by the truth of A~ B 1 and the axiom tiMPLIES (AND A B) C). If ~ 1s made false by a planned action, it is necessary to refute the conjunction. Since both A and B were true (before the action) it is indeterminate whether one or both should' be changed. London outlines two approaches to the problem of local indeterminacy: the intro­ duction of uncertainty into the network bv allowing the propagation of a TV for "unknownr' to refute the support for both A and B or else by r equiring domain knowledge to b~ suffi­ C1en tiy complete and, moreover, suitably expr essed to determine with certainty all consequences of a state change (by forward (an­ tecedent) inference). These alternatives are gene rally unacceptable, but the method dis­ cussed here offers less sensitivity to the structure of domain axioms and avoids the introduction of uncertainty in most cases.

London pointed out that, in the case of refuting conjun~tive support, the spread of uncer tainty can 1n some cases be mitigated by ne~ lines of support emanating from the state or1ginally changed, as would occur in the case of "exhaustive support" with complete domain knowledge (4]. Since with incomplete knowledge such new support is not guaranteed to propagate to t he refuted conjunction, some uncertainty may still remain In the net. By using a mul­ tiple-level agenda mechanism, the ERIS system defers the propagation of uncertainty to a queue with lower priority than that for known truth values so that a line of support may be found that eliminates the uncertaintv without having to mark nodes as "unknown'' unneces­ saril y.

Furthermore, unlike London's system the CC method provides a wav to undo the labelling of nodes marked "unknown'' in the event that uncer­ taint y propagates to a well-founded consequence of the original state change or if uncertainty was s pread to nodes in a conjunctive antecedent and subsequently one of the nodes was found to hav~ a known refutation. This is accomolished in part by allowing well-founded TV's to override the "unknown" TV even within the CC and also by retracing the spread of uncertainty when needed to reconstruct previous support. The CC method has the additional ability to detec t instances where multiple antecedents are not linked by the same connective, but in which the network is globally indeterminate following a change .

The remaining difficulty encountered in modelling is the problem of capturing all the consequences of a state change. The above dis­ cussion pertains to instantiated structure with initially known truth values, but it is often necessary to invoke deduction to determine whether nodes that could possibly have been providing support before the state change (due t? ~nresolved uncertainty) were in fact pro­ V1dlng support. If such nodes were supporting a s~ate that is changed by an action then the1r ~upport must also be refuted. Faiiure to determ1ne the support status of indeterminate nodes with respect to a changed state may cause some of the consequences of an action to be ignored. This is the problem of exhaustive suP.port, as desc~ibed by London [4] and is a maJ?r problem 1n dependency-based modelling . It 1s related both to the completeness of the domain knowledge ~d to deductive s~arch, since the basic problem 1s that of prov1ng a uni­ versal, namely the completeness of the set of consequences (or the non-existence of a line of support from the action consequent to any sup­ posedly unaffected state). The problem of the completeness of domain knowledge is outside the scope of the system (although indeterminacy following a state change may allow it to detect 1ncompleteness). Deducing the TV's of previ­ ously unknown states to determine their support status may place large demands on the deductive component.

3 . Concluding Remarks

By allowing logical support to be determined w1thin existing structure, the restriction that dependencies be explicitly declared in clause form is eliminated. This is accomplished by connective specialists that use graph labelling to maintain consistency in the network 1 greatly reducing the overhead for symbol man1pulation required by the deductive process, as rewrite rules are also eliminated (except for the initial simplification of expressions). The creation of new structure is limited to the instantiation of rules during deduction. By avoiding the structural manipulation of exp,res­ s~ons the network becomes in effect, a 'com­ p1led'l knowledge rerresentahon' upon which the procedural special sts operate merely by the propagation of normal and "meta" truth value "signals".