Modal Propositional Semantics for Reason Maintenance Systems

MODAL PROPOSITIONAL SEMANTICS FOR REASON MAINTENANCE SYSTEMS*

Allen L. Brown, Jr. General Electric Corporate Research and Development Schenectady, New York 12301 Arpanet: BrownAL @GE-CRD

ABSTRACT

Non-monotonic logics are examined and found to be inadequate as descriptions of reason maintenance sys­ tems (sometimes called truth maintenance systems). A logic is proposed that directly addresses the problem of characterizing the mental states of a reasoning agent at­ tempting to reason with respect to some object theory. The proposed logic, propositional dynamic logic of derivation (PDLD), is given a semantics, and a sound and complete axiomatization. The descriptive power of PDLD is demonstrated by expressing various inferential control policies as PDLD formulae.

In this note I will elaborate the propositional frag­ ment of an axiomatic semantics of reason maintenance systems (RMS's) [Do2l. The development of such a se­ mantics stems from the desire to provide a declarative specification language for RMS's with particular em­ phasis on the description of the control of their reason­ ing processes, and to serve as a formal setting within which to compare and contrast the properties of different RMS's.

I. INTRODUCTION

There is considerable ongoing research activity in the realm of non-monotonic reasoning [Pel . The· avowed aim of this research is to capture in a logical formalism some of the non-monotonic processes (e.g., default rea­ soning and defeasible reasoning) that are clearly part of the common sense reasoning repertoire enjoyed by hu­ mans. Implicit or explicit in many of these formalisms is the notion that the formalism in some sense describes the process carried out by the reasoning agent. McDermott and Doyle [McDDo) analyze Doyle's TMS [Doll in terms of the non-monotonic logic that they elaborate. Their analysis suggests that the logic of TMS is a fragment of their non-monotonic logic. I believe that their analysis confuses the logic practiced by the reasoning agent (the TMS) with the particular object theory that the agent reasons about. A reasoning agent should be viewed as a finitary computing entity. The computations that it carries out have the express aim of mechanizing some object theory. Depending on the na­ ture of the object theory or the reasoning agent's grasp

· The research reported herein is funded in part by the Defense Advanced Research Projects Agency under contract number F30602-85-C-0033.

of the theory, the mechanization may turn out to be im­ perfect. With respect to logics like that of [McD 1 and [Re), because there cannot be, in general, a recursive enumeration of the theorems of the object theory, a reasoning agent's mechanization of such theories is bound to be imperfect. In summary, the relation that obtains between an object theory and a reasoning agent is that the theory is an ideal object that the agent might hope to compute.

The sense in which many of the non-monotonic log­ ics that have been studied might be descriptions of RMS's, or reasoning agents more generally, is roughly the sense in which a formalization of recursive function theory might be the description of a programming language, say PASCAL. Recursive function theory can be taken as an ideal object that a PASCAL implementa­ tion attempts to mechanize. However, recursive func­ tion theory has little to say about the actual semantics of PAS CAL programs. Inevitably, a formal semantics of PAS CAL would include recursive function theory, but most of the meat in axiomatizing PASCAL is the for­ malization of the states of the abstract machine that is interpreting PAS CAL.

There are some researchers who have attempted to address the issue of describing the reasoning agent and its mental states. Weyhrauch's FOL system [We) has an explicit notion of object theory and meta-theory. (Indeed, FOL permits the construction of arbitrary hierarchies of such object/meta pairs.) FOL is an ax­ iomatic system, specifically, a first-order system with types. From my perspective, FOL's main defect is that a FOL meta-theory, if taken as an attempt to formalize the properties of reasoning agents, has no explicit no­ tion of the agent's mental state. I believe that an explicit notion of mental state is key to many representations and control issues.

Doyle [Do2) develops a very powerful functional se­ mantics for theories of reasoned assumptions. His se­ mantics, in the guise of an admissible set, has a definite notion of the mental state of a reasoning agent. He ela­ borates his functional semantics so as to be able give taxonomic structure to a wide range of reasoning for­ malisms. He focuses primarily on giving an account of what inferential theories are sanctioned by different for­ mal notions of reasoned assumptions. My interest, in contrast, is in describing the behavior of a reasoning agent when constrained to adhere to particular object theories. I should also mention that I prefer axiomatic to functional specifications as I think there is much more available technology for compiling operational RMS's from axiomatic descriptions.

Goodwin recently introduced [Go] a new inferential formalism, logics of current proof (LCP's). His intent is to capture the dynamic reasoning processes of finite rea­ soning agents. LCP's are not logics in the usual sense as they have no proof theory or model theory. Goodwin's formal account of LCP's is functional in nature. The principal appeal of LCP's is that they explicitly encode the development of the deductive process. It was in at­ tempting to give a first-order logic account of LCP's, having models that suitably interpreted the sequence of databases in an LCP that I happened upon the idea of a dynamic logic of derivation.

The proximal technical inspiration of the dynamic logic of derivation (DLD) is the dynamic logic (DL) formalism introduced by Pratt and elaborated by Fisch­ er, Hare!; Ladner, Meyer, and others [Hal , Ha2l. DL gives axiomatic meaning to programs by means of a first-order language augmented with a collection of modal operators corresponding to those programs. For­ mulae in the language are used to characterize the states of computational processes before and after the execu­ tion of some computational step(s). DL's model theory is a collection of Kripke-style worlds [HeCr] connected by binary relations corresponding to various possible programs. Just as the worlds of DL's semantics capture the states of a computational machine, the states of a DLD model will capture the mental states of a rational agent. The approach that I shall be taking is presaged by Pratt in [Pr] where he uses .variants of DL to formalize individual actions, sequences of actions (processes), and their effects. The remainder of this paper is devoted to elucidating propositional dynamic logic of derivation

(PDLD) .

II. SYNTAX

Let L be a first-order language equipped with func­ tions, predicates, connectives, quantifiers, and perhaps even modalities. L has the usual formation rules for first-order languages. The details of L will not concern me very much here. Let T be a theory over the language L. T is assumed to be axiomatizable with a set of axioms and rules of inference. 'L, the language of PDLD, can to some extent be considered a meta­ language for for theories over L. Formulae over 'L will typically be used to specify how the formulae of T are actually derived from T's axioms and rules of inference. This specification will be in the form of an axiomatized

theory 'T. I will call 'T the mechanization of T. In effect

'T, when so elaborated, will (partially) specify a reason maintenance system for the theory T .*

'L has two sets of symbols: the atomic formulae and the atomic derivations. The atomic formulae are further subdivided into two classes, the proper atomic formulae and the reified atomic formulae. '<1> is a reified atomic formula of ' L if, and only if, <1> is a formula of L. I will use (possibly subscripted) q,, .p, and x to denote formula variables of L ; <1>, 'I', and X to denote instances of for­ mulae of L; p, q and r to denote formula variables of 'L; P, Q, and R to denote instances of atomic formulae of' L; a and 13 to denote derivation variables; and a and b to denote instances of named atomic derivations. There is also the anonymous atomic derivation, f- . The proper atomic formulae are meant to behave like the truth value bearing constants of ordinary proposi­ tional logic. Intuitively reified atomic formulae are for­ mulae that are asserted as deduced after some instance of a rule of inference in T has been applied.** Similarly atomic derivations are specific instances of inference rules. The PDLD-wffs and PDLD-derivations are defined by simultaneous induction:

1. an atomic formula is a PDLD-wff,
2. an atomic derivation is a PDLD-derivation,
3. for any PDLD-derivations a and 13 (a;l3), (aU 13), a·, and a- 1 are PDLD-derivations,
4. ·
5. for any PDLD-wffs p and q and PDLD­ derivation a , ...,P, pVq, and <a> p are PDLD­ wffs.

I will abbreviate ...,(...,pV...,q) to pl\q; ...,pVq to p--+q; (p-q)l\ (q-p) to p=.q; <a;a "- 1 >p (n>O) to <a">p; ...,<a>...,p to [a]p; and <a 0 >p top.

III. SEMANTICS

Let W be a non-empty universe of states, elements of which are denoted by s and t (possibly with sub­ scripts) . A PDLD interpretation determines whether or not an PDLD-wff P is true in a state s (or s satisfies P) . Atomic derivations can be viewed as binary relations on W. Accordingly an interpretation is defined to be a triple < W,1T,m> , where w is a non-empty set, 1T is a function from the atomic formulae into 2 w, and m is a function from the atomic derivations into 2 wx w. 1T and m provide meaning for atomic formulae and derivations, and are

extended inductively to the rest of 'L:

· I wish to distinguish PDLD (and the first-order dynamic logic of derivation) from the dynamic logics of programs investigated by Pratt et al. The distinction is not grounded so much in their respective model theories or proof theories, but rather in the fact that the model-theoretic worlds of the former are related by program statements while in the latter they are related by inferential steps.

·· The distinction between proper and reified atomic formulae will play no role in the development of PDLD proper. The distinction becomes important when the

axioms that describe part icular RMS's are adjoined to the axiomatization of PDLD.

Denoting sE7T(P) by s FP and <s,t>Em(a) by sat and adopting free usage of conventional logical symbols, one may write for a fixed interpretation < W,1r,m> that s I= <a> P if, and only if, there is a t such that sat and tl= P. Given an interpretation S=< W,1r,m>, a PDLD-wff P is S-valid (written p 5P) if for every sEW sf= P. A PDLD-wff P will be said to be PDLD­ valid (written f=P) if for every s, it is S-valid. P will be said to be S-satisfiable if there is an s such that s f= P. and satisfiable if there is an s such that l=sP.

IV. AXIOMATIZATION

The axioms '{ P)' through '{Bew)' together with the rules '{MP)' and '{Nee )' below form the system P. The axioms for P are:

• {T*) the tautologies of propositional calculus

The rules of inference for P are:

The following two theorems are straightforward conse­ quences of the syntax, semantics, and axiomatization above:*

Theorem: The axioms '{T*)' through '{Bew)' are PDLD­ valid.

Theorem: The rules of inference '{MP)' and '{Nee)' are sound with respect to PDLD interpretations.

Parikh's completeness proof for propositional dynamic logic of programs [Pal can be adapted to PDLD to ob­ tain:

Theorem : Every PDLD-valid formula is in the deductive closure of the system P . **

V. DESCRIPTIVE POWER

A. General Considerations on Monotonic Theories

Thus far I have done nothing that connects any par­ ticular object theory T with a mechanization 'T. To make that connection and to exhibit the descriptive power of 'L, I will augment P with proper axioms that characterize a monotonic theory T. Assume that T in­ cludes the first-order predicate calculus. For each axiom <I> of T, there is an axiom '<I> of 'T. Consider an in­ stance of modus ponens in T:

This suggests an axiom for 'T of the form:

· Proofs of theorems may be found in [Br] .

.. The principal technical hurdles in adapting Parikh 's complex proof to P are in validating certain claims that Parikh makes for "pseudo-models" and " closed sets" when applied to P .

··· For a complete characterization of a monotonic inference rule such as modus ponens one should also add the axiom 'Pf\'(P- Q) - [MP]'Qsince the rule is ent irely deterministic in its consequent.

The second observation to be made about modus ponens is that it is "belief conserving." That is, any­ thing that is believed before the application of modus ponens should continue to be believed afterward. Con­ servation of belief (and non-belief) is a property in­ herent in monotonic rules of inference. To generalize then from the case of modus ponens, for each inference instance (of r) represented by the atomic derivation a with antecedents <1>~, ... ,<1>" and consequent 'I' there is an axiom of 'T of the form

Given that T is monotonic, it seems natural to require the following frame axiom schema to enforce belief con­ servation relative to each atomic derivation:

It can be shown that < f---'> '<I> can be proved from 'T (keepirig in mind that 'T mechanizes the first-order predicate calculus) , an augmentation of P, whenever <I> is a theorem of T. Indeed, P augmented with a axioms corresponding to an object theory T together with derivation and frame axioms as above will be termed the natural mechanization of r. This leads to asserting that a PDLD theory 'T completely mechanizes T just in case

Needless to say, if the object theory T to be mechan­ ized happened to be the pure first-order predicate cal­ culus, formulae such as -o< r'> '<I> cannot generally be proven in the natural mechanizing theory 'T [Bo). This observation has important consequences vis a' vis the proof theory of non-monotonic theories [McD) and their mechanizations (see below) .

Notice that for an object theory T and mechanizing theory 'T, . I have been implicitly taking < r '>'<I> to mean that 'T "believes" '<I> to be a consequence of believing the object theory T. Suppose P were taken as the object theory of 'T. *** 'T can be constructed in such a way that <I> is a theorem of 'T if, and only if, < at; ... ;an> '<I> is a theorem of 'T for some sequence at. ... ,a" of (reified) atomic derivations. On the other hand, it can also be demonstrated for 'T that <I> is not a theorem of 'T if, and only if, < a1; ... ;an> '<I> is not a theorem of 'T for any sequence at. ... ,an of atomic derivations. In fact, <I> is not a theorem of ' T if, and only if, ....,'<l>--+<a1; ... ;an>....,'<l> is a theorem of 'T for every sequence at. ... ,a" of reified atomic derivations. The situation that appears to obtain in 'T then is the PDLD analogue of what Moore [Mol calls autoepistem­ ic stability of an ideally rational agent. Loosely speak­ ing, <I> is a theorem of 'T if, and only if, from every mental state (wherein <I> may or may not believed) there is a derivation leading to a mental state in which <I> is believed. Conversely, <I> is not a theorem of 'T if, and only if, (dis-)belief in <I> is invariant under deriva­ tion.

· The assertion < f-:' > <P does not suffice on the right hand side of the " if, and only ir' as T might be a non-monotonic theory. The second clause is necessary in order to assure that once ' T derives '<ll it "sticks" and that ' T does not osci l­ late, believing and disbelieving '<t> , owing to some belief revision policy.

·· To see how such a thing is possible, let ' L be the language L together with the formula '<!» whenever <J> is a formula of ' L . Consider 'P, the system P taken over 'L together ·with an axiom '<t> whenever <t> is an ax iom of P , the natural axiomatic encodings of the rules of inference (modus ponens and necessitation) of P , and the frame axioms for those rules of inference. In the same spirit as reified atomic formulae, atomic derivations that are instances of modus ponens

and necessitation of the system P will be called reified.

B. Specifying Breadth-first Search

An explicit derivation of <I> is a formula of the form <a1; ... ;ak>'<l>. 'T enumerates the theorems ofT in a breadth-first fashion if and only if

1. for each theorem <I> of T, there is an explicit derivation of <I> that is a theorem of 'T,
2. the sequence of named atomic derivations that appears in the prefix of '<I> corresponds to the sequence of inference rules applied in the proofs of the theorems of T when enumerating them in breadth-first order,
3. if 'I' t precedes '1'2 in the breadth-first ordering, then the derivation of '1'2 cannot be proved as a theorem of 'T until 'I' t has been proved.

A formula T is said to be of rank n if the shortest proof of that formula is of length n. Then axioms of T are of rank 0. Let~" be an ordered list of the last atom­ ic derivations applied in the proofs of each of the for­ mulae of rank n. * Breadth-first enumeration is achieved by replacing axioms '(a}' above with '(an,ml' below:

and adding boundary conditions

where the an.m is the m 'th atomic derivation on the list ~ "' and the <I> n,m 's and 'I' n,m are, respectively, the an­ tecedents and consequent of the atomic derivation an,m·

· It could be that the formulae of rank n are infinite in number. In that case the enumeration will never get beyond the formulae of rank 11.

The interaction of the C's and D's prevents 'I' n,m from being derived before 'I' n,m+l is derived. Indeed, no for­ mula of rank n is derived before every formula of lesser rank is derived. The 'I' 's are thereby forced to be pro­ duced in breadth-first order. Of course it must be verified that a theory 'T that mechanizes T completely, when modified with the breadth-first axioms, continues to mechanize T completely. To that end the following holds:

Theorem: If 'T is the natural mechanization of T with ax­ ioms '{a}', and if 'T' is the breadth-first mechanization of T with axioms '{a. m)' and '{Ba. m)' replacing '{a}', and if G < f-' > '<I>, th~n f-;T. < f-' > ·<I> .

With a different set of boundary conditions, a depth­ first enumeration of the theorems of T could have been achieved. That is, there is a set of boundary conditions such that

1. for each theorem <I> of T there is an explicit derivation of <I> that is a theorem of 'T,
2. the sequence of named atomic derivations that appears in the prefix of '<I> corresponds to the sequence of inference rules applied in the proofs of the theorems of T when enumerating them in depth-first order,
3. if 'I' 1 precedes 'I' 2 in the depth-first ordering, then the derivation of 'I' 2 cannot be proved as a theorem of 'T until 'I' 1 has been proved.

The interaction between the axioms '{a ·. ml' and bound­ ary conditions suggests a general "programming" meth­ odology for controlling the application of derivations. The propositional constants Dn,m and c ·. m should be viewed as "enabling" and "completion" flags for the firing of the atomic derivation an ,m· These constants in­ dicate respectively that a derivation can be used and that a derivation has been used. Programming then consists of designing systems of boundary conditions to achieve the desired sequencing of inferences by suitably control­ ling the truth values of enabling flags in various mental states.

Goodwin [Go] (and McDermott before him in [McD]) cites a number of problems in using deduction to control deduction. He remarks that attempts at con­ trolling inferences by deductive methods have typically resulted in invalidating particular inferences altogether, or alternatively resulted in RMS states that assert that some proposition has been proven if and only if it has not been proven. It should be clear from the discussion of programming above that atomic derivations are en­ abled with respect to particular states. As a conse­ quence, an inference can be temporarily en-(dis-)abled, and there is no problem whatsoever in having some pro­ position ''I' be derived by some derivation that has since become disabled. The axioms '{Ba ·. ml' could just as well have been written

which have the effect of disabling each of the '{ a ·. ml' after use.

C. Finite Reasoning Agents

At the outset of this note I proclaimed PDLD as a mechanism for describing the behavior of finite reason­ ing agents. Careful scrutiny of PDLD interpretations will reveal that PDLD theories admit interpretations which are at odds with any reasonable notion of a finite agent. Consider the following observations: If one thinks of a sequence of mental states related by various atomic derivations as corresponding to the flow of some sort of mental time, then time can extend infinitely into the past and future. Moreover, a mental state can be im­ mediately preceded by multiple states. Finally, states can be "dense." That is, PDLD interpretations can be such that for an atomic derivation a whenever < s, t > Em (a) there is au such that <s,u>Em(a) and <u,t>Em(a) .

As it turns out, all of these anomalies can be legislat­ ed away with appropriate axioms. Tense logics [RU] that impose various topologies on the ordering of time pro­ vide much of what is needed. To focus on one of the anomalies, consider the infinite extension into the past. This can be eliminated with:

This last formula says that every state either is, or is preceded by, a state which is not immediately preceded by a state that satisfies pV-.p. But since every state satisfies pV...,p, this formula can be satisfied if, and only if, every state is either immediately preceded by no state at all, or is preceded by some state which is in turn pre­ ceded by no state. This axiom prevents infinitely long (receding) chains of states. On the other hand, it does not prevent interpretations having a particular state from which there is a receding chain of any given finite length. More axiomatic machinery still is required to prevent that.

D. Non-monotonic Theories

In considering the descriptive power of PDLD with respect to non-monotonic theories it should first be not­ ed that the intuitive statement of the rule of possibilita­ tion introduced in [McDDo] is directly expressible in PDLD. Recall that McDermott and Doyle first gave an informal definition of their non-monotonic rule of infer­ ence which stated that if a proposition were not provable in a theory T, then the negation of the proposition is provably possible. Though the intent of this rule is clear, it is unfortunately circular. McDermott and Doyle had to appeal to an indirect technical device to capture possibilitation. In the PDLD mechanization of T, how­ ever, their original notion of possibilitation can be ex­ pressed as:

where '0' is the consistency modality of [McDDo, McD]. Possibilitation is well defined but, unfortunately, not effectively computable in general. Since there is no magic, a non-monotonic theory T that is not recursively enumerable, cannot have a complete mechanization that is recursively enumerable. If a (partial) mechanization 'T is to remain r.e., such mechanizations cannot in gen­ eral have the formulae ..,< ~·> '..,¢ (on the antecedent side of '{Pos} ') as theorems.

The whole point of a non-monotonic logic is to for­ malize the default and defeasible inferences that are evi­ dent in common sense reasoning and practiced by vari­ ous RMS's. It should be evident that POLO provides a mechanism for directly formalizing such reasoning without necessarily resorting to the sorts of infinitary processes implicit in McDermott and Doyle's rule of possibilitation. In order to realize defeasible inferences, a PDLD theory cannot have the general frame axioms '{aF) '; not all atomic derivations will be belief conserv­ ing. A default introducing axiom scheme might be:

which says that if ""'¢ is not currently believed then ¢ can be believed. Of course, it might be the case that h-r < 1--·> '-.¢. Thus, the simple notion of default rea­ soning supported by '{Hyp)' would admit states to in­ terpretations of 'T that sanctioned inconsistent beliefs. Now for 'T to have inconsistent beliefs is not the same as 'T's being inconsistent. On the other hand, states that have '¢/\ '..,¢ true are irrational, and to have < f-·> '¢/\'..,¢ as a theorem of 'T makes 'T irrational. RMS's generally have backtracking mechanisms to re­ vise the set of current beliefs so that consistency of be­ liefs is restored. Although PDLD as presented here is not expressive enough to describe all the details of those mechanisms, it can describe the general policies that are typically enforced by those mechanisms. A weak policy might be:

which says that if the reasoning agent is in a state that is irrational with respect to a particular formula ¢, all states immediately reachable from that state should be rationalized. A much stronger (and typically unenforce­ able by effective computation) policy is stated by:

'This formula says that if the reasoning agent is in a state that is irrational with respect to a particular formula ¢, the agent should do something (e.g., withdraw sufficient premises or hypotheses in which the irrational state is grounded) such that at no future time can the agent be in a state irrational with respect to ¢. These examples of deduction and premise control policies seem to respond directly to McAllester's [MeA] objections to non­ standard logics:

The problem with non-monotonic logics is that they bring in non-traditional formalisms too early, muddy­ ing deduction, justifications, and backtracking. The aspect of truth maintenance which cannot be formal­ ized in a traditional framework is premise control ...

Dynamic logics of derivation offer an opportunity to make the various issues explicit.

VI. CONCLUSIONS

In the foregoing I have developed the syntax and se­ mantics of the propositional dynamic logic of derivation, and presented a complete axiomatization for the logic. By way of examples I have illustrated some of the ex­ pressive power available in PDLD for specifying and analyzing the behavior of reason maintenance systems. Finally I have offered dynamic logic as an alternative to the sorts of non-monotonic logics investigated hereto­ fore as a means for giving a formal account of some as­ pects of common sense reasoning.

PDLD obviously cannot be .completely expressive of all properties that might be ascribed to an RMS. For that, one requires the first-order dynamic logic of derivation [Brl. In the latter formalism one can not only give a complete first-order account of control protocols, but also of the collateral data structures (viz. "no-good" lists, hypothesis contexts, dependency relations, etc.) that RMS's utilize in the belief revision process. Be­ tween PDLD without the I-· derivation and full 'first­ order dynamic logic of derivation there are many alter­ native logics having different powers of expressiveness. The analogous dynamic logics of programs have been extensively investigated. I believe that those investiga­ tions will offer a good starting point for developing an RMS specification logic which is suitably expressive, while being deductively tractable.