A Deductive Model of Belief

1. Introduction

As AI planning systems become more complex and are applied in more unrestr:icted domains that contain autonomous processes and planning agents, there are two problems (among others) that they must address. The first is to have an adequate model of the cognitive state of other agents. The second is to form plans under the constraint of resource limitations: i.e., an agent does not always have an infinite amount of time to sit and think of plans while the world changes under him; he must act. These two problems are obviously interlinked since, to have a realistic model of the cognitive states of other agents, who are presumably similar to himself, an agent must reason about the resource limhations they are subject to in reasoning about the world.

In this paper we address both problems with reference to AI planning system robots and one part of their cognitive state, -;·amely beliefs. Our goal is to pursue what might be called robot psychology : to construct a plausible model or robot beliefs by examining robots' internal representations of the world. The strategy adopted is both descriptive and constructive. We examine a generic AI robot planning system (from now on we use the term agent) for commonsense domains, and isolate the subsystem that represents its beliefs. It is then possible to form

1 This paper describes results from the author's dissertation research. The work presented here wa.e supported b;r grant NOOH--80-C~6 from the Office of Naval Research.

A DEDUCTIVE MODEL OF BELIEF

Kurt Konolige

Artificial Intelligence Center SRI International

an abstraction or the agent's beliefs, that is, a model or what the agent believes. This is the descriptive part of the research strategy. Among the most important properties of this model is an explicit representation or the deduction or the consequences of beliefs, and so we call the model one of Deductive Belief.

It is assumed that the beliefs of the agent are about conditions that obtain in the planning domain, e.g., what (physical) objects there are, what properties they have, and what relations hold between them. Thus the descriptive model of Deductive Belief has an obvious shortcoming. Although agents can reason about the physical world, they don't have any method for reasoning about the beliefs of other agents (or their own). By t.aking the descriptive model to be the way in which agents view other agents' ·beliefs, we can construct a more complex model of belief that lets agents reason about others' beliefs. This is the constructive part of the research strategy.

There are two main sections to this paper. In the first, the concept of a belief subsystem is introduced, and its properties are defined by its relationship to the planning system as a whole. Here we discuss issues of deductive closure, completeness, and the resource limitations of the belief subsystem. We also characterize the constructive part of the model by showing how to expand a belief subsystem to reason about the beliefs of other · agents. In the second section, we formalize the Deductive Belief model for the propositional case by introducing the belief logic B, and compare it with other formalizations of knowledge and belief. Because the treatment here must be necessarily brief, throughout the paper proofs established by the author, but not yet published, are referenced.

2. Deductive Belief

What is an appropriate model of belief for robot problem­ solving systems reasoning about the world, which includes other robot problem-solving systems! In this section we discuss issues surrounding this question and propose a model of Deductive Belief as a suitable formal abstraction for this purpose.

2.1 Planning and Belief: Belief Suba)'atema

A robot planning system, such as STRIPS, must represent knowledge about the world in order to plan actions that affect the world. or course it is not possible to represent all the complexity of the real world, so the planning system uses some abstraction or real-world properties that are important for its task, e.g., it might assume that there are objects that can be stacked on each other in simple ways (the blocks-world domain). It is helpful to view the representation and deduction of facts about the world as a separate subsystem within the planning system; we call it the belief su.bsystem. In its simplest, most abstract form, the belief subsystem comprises a list of sentences about a situation, together with a deductive process for deriving consequences of these sentences. It is integrated with other processes in the planning system, especially the plan derivation process that searches for sequences of actions to achieve a given goal.

In a highly schematic form, Figure 1 sketches the belief subsystem and its interaction modes with other processes of the planning system. The belief system is composed of the base sentences, together with the belief deductive process. Belief deduction itself can be decomposed into a set of deduction rules, and a control st.rategy that determines how the deduction rules are to be applied and where their outputs will go when requests are made to the belief subsystem.

There are two types of requests that result in some action in the belief subsystem. A process may request the subsystem to add or delete sentences in its base set; this happens, for example, when the plan derivation process decides what sentences hold in a new situation. Although this process of belief updating and revision is a complicated research problem in its own right, we do not address it here (see Doyle [1] for related research). The second type of request is a query as to whether a sentence is a belief or not. This query causes the control strategy to try to prove that the sentence is a consequence of the base set, using the deduction rules. It is this process of belief querying that we model in this paper.

We list here some further assumptions about belief subsystems. The internal language of a belief subsystem is a formal language, which must include a (modal) belief operator, e.g., a propositional or first-order modal language would be appropriate. It is assumed that there is a Tarskian semantics for the language, that is, sentences of the language are either true or false of the real world. The belief subsystem doesn't inherently support the notion of uncertain beliefs, although this idea could be introduced if the internal language contained statements about uncertainty, e.g., statements of the form Pis true with probability 1/2.

The deduction rules of a belief subsystem are assumed to be sound (with respect to the semantics of the internal language), effectively computable, and to have bounded input. In particular, this forces deduction rules to be monotonic. It is our view that nonmonotonic or default reasoning should occur in the belief updating and revision process, rather tha~ in querying beliefs.

The process of belief derivation is assumed to be total. This means that the answer to a query will be returned in a finite amount of time; i.e., the belief subsystem cannot simply sit and continue to perform deductions without returning an answer.

It is possible to define several types of consistency for beliefs. Deductive consistency requires that no sentence and its negation be simultaneous beliefs. Logical consistency requires that there be a world in which all the beliefs are true. Note that deductive consistency does not entail satisfiability, because the deductive process may not be complete. That is, a set of beliefs may be unsatisfiable and thus logically inconsistent, but, because of resource limitations, it may be impossible for an agent to derive a contradiction. Deductive consistency is the appropriate concept for belief subsystems. The assertion that rational agents are consistent is compatible with, but not required by, the model. It gives rise to a slightly different axiomatization (see Section 3).

The results of this paper depend only on the most general features of a belief subsystem as depicted in Figure 1: namely, that there is a formal internal language in which statements about the world are encoded; that there is a finite set of base belit>fs in this language; and that there is some process of belief deduction that applies w"und and eff~ctively computable deduction rules to the base sentences at appropriate times, in response to requests by other processes in the planning system. A belief subsystem with these properties (along with the amplifications and restrictions given above) is a model of belief for planning agents, which we call Deductive Belief.

2.2 Resource Limitations and Deductive Closure

One of the key properties of belief deduction that we wish to include is the effect of resource limitations. If an agent cannot deduce all the logical consequences of his beliefs, then we say that his deductive process is incomplete. Logical incompleteness arises from two sources: an agent's deduction rules may be too weak, or his control strategy may perform only a subset of the derivations possible with the deduction rules. Both these methods can be, and are, used by AI systems confronted wit.h planning tasks under strict resource bounds. For several reasons, both conceptual and technical, we do not include incomplete control strategies in the Deductive Belief model. Instead, we make the following assumption:

CLOSURE PROPERTY. The sentences derived in a belief subsystem are closed under its deduction rules.

One advantage of requiring that beliefs be closed under deduction is conceptual clarity and predictability. If beliefs are not closed, then there is some control strategy that guides the deductive process, making decisions to perform or not to perform deduct.ions. If this control strategy uses a global effort bound, then behavior of such a subsystem is hard to predict. Theoretically there may be a derivation of a sentence, but the control strategy in a particular case decides not to derive it, because it tried other derivations first. Closed systems, on the other hand, behave more dependably. They are guaranteed to arrive at all derivations possible with the given deduction rules.

The concept of "belief" is also complicated by the introduction of control strategy issues. For example, it makes a difference to the control strategy as to· whether a sentence is a member of the base set, or obtained at some point in a derivation . . One cannot simply say, "Agent S believes P," because such a statement doesn't give enough information about P to be useful. If P is derived at the very limit of deduction resources, then nothing will follow from it; if it is a base sentence, then it might have significant consequences.

In terms of formalizing the model of Deductive Belief, the assumption of closure is technically extremely useful. Consider the task of formalizing a belief subsystem that has a complex global control strategy guiding the deductive process. To do this correctly, one must write axioms that describe the agendas, proof trees, and other data structures used by the cont.rol strategy, and how the control process guides deduction rules operating on these structures. Reasoning about the deductive process involves making inferences using these axioms to simulate the deductive process, a highly inefficient procedure. By contrast, the assumption of closure leach to a simple formalization of belief subsystems that incorporates the belief deductive process in a direct way (the Deductive Belief logic, B, is presented in the next section). We have found complete proof techniques forB that involve running an agent's deductive system directly, in a manner similar to the semantic attachment methods of Weyhrauch [6].

Having argued that control . strategies that use a global effort bound are undesirable, we now show that weak (but closed) deduction can have the same effect as control strategies with a local effort bound. We define a local bound as a restriction on the type of derivations allowed, without regard to other derivations in progress, i.e., all derivations of a certain sort are produced. An example of this sort of control strategy is level-saturation in resolution systems. Here we give a simpler example.

Suppose an agent uses modus ponens as his only deduction rule, and has a control strategy in which only derivations using fewer than k applications of this rule are computed; this is a local effort bound. To model this situation with a closed belief subsystem, consider transforming the base set so that each sentence has an extra conjunct tacked onto it, the predicate DD(O)(DD stands for "derivation depth"). Instead of modus ponens, the belief subsystem has the following modified deduction rule:

M P2 is sound and effectively computable, so it is a valid deduction rule for a belief subsystem. The closure of the base set of sentences of the belief subsystem under M P2 will be the same (modulo the DD predicate) as the set of sentences deduced by the nonclosed control strategy of the agent.

The Closure Property, together with the assumption of totality for the belief derivation process, imply that the deduction rules are decidable for all base sets of sentences.

2.3 Views

Up to this point, we have specifically assumed that agents don't have any deduction rules dealing with the beliefs of other agents . Now, however, we form the constructive part of the Deductive Belief model: adding to the belief subsystem model so that an agent can reason about its own and other belief subsystems.

We can arrive at deduction rules that apply to beliefs by noting that the obvious candidate for the intended interpretation of the belief operator is another belief subsystem. That is, the modal sentence [S]o is intended to mean "the sentence o is derivable in agent S's belief subsystem." The new deduction rules that apply to belief operators will be judged sound if they respect this intended interpretation. For example, suppose a deduction rule states that, from the premise sentences [S]p and [S](p =>q), the sentence (S]q can be concluded. This is·a sound rule if modus ponens is believed to be a deduction rule of S's belief subsystem, since the presence of p and p=>q in a belief subsystem with modus ponens means that q will be derived.

We summarize by postulating the following property of Deductive Belief:

RECURSION PROPERTY. The intended model of the belief operator in the internal language of a belief subsystem is another belief subsystem. The intended model for an agent's own beliefs is his own belief subsystem.

The Recursion Property of belief subsystems leaves a large amount of flexibility in representing nested beliefs. Each agent might have his own representational peculiariaties for other agents' beliefs. An agent John might believe that Sue has a set of deduction rules Rt, whereas he believes that Kim's rules are R2 · In addition, John might believe that Sue believes that Kim's rules are R3 . We call a belief subsystem as perceived through a chain of agents a view, and use the Greek letter 11 to symbolize it. For example, John's perception of Sue's perception of Kim's belief subsystem is the view 11 = John,Sue,Kim.

Obviously, some fairly complicated and confusing situations might be described with views, in which agents believe that other. agents have belief subsystems of varying capabilities. Some of these scenarios would be useful in representing situations that are of interest to AI systems, e.g., an expert system tutoring a novice in some domain would need a representation of the deductive capabilities of the novice that would initially be less powerful and complete than its own, and could be modified as the novice learned about the domain.

Having stated the Recursion Property, we now ask if there is a way to implement it within the confines of belief subsystems. At first glance it would seem so: suppose the agent S wishes to know whether he believes some statement p, i.e., whether (S)p is one of his own beliefs. If we assume he can query his belief subsystem, he simply submits p to it; if it answers "yes," he believes [S]p, and if "no," then he believes ~[S]p. Similarly, if he wishes to know whether another agent S' believes p, he simply queries a subsystem supplied with (his version of) S' deduction rules, and uses the answer to conclude either [S']p or ~(S']p.

The problem with this strategy is that we haven't shown that Swill receive an answer from the subsystems he queries. In the case of querying his own subsystem, there may be another occurrence of the modal operator [S] that will cause a recursive call to his belief subsystem, and so on in an unbounded manner. Although we assumed that the initial subsystem without the Recursion Property was decidable, we have not shown that this is also true for the expanded subsystem.

In the case of querying S''s subsystem, S doesn't have the complete subsystem in hand, since he has incomplete knowledge of the base set. So, in effect, S must try to prove that, in each of S''s base sets that are consistent with S's beliefs, p is derivable. But even if we assume that individual subsystems that faithfully implement the Recursion Property are decidable, we haven't shown that the theory of a set of such subsystems is decidable, which is what is needed for S to receive an answer to (S')p.

We now give a formal interpretation of these issues. Let 6 be a belief subsystem for agent S characterized by a set of deduction rules R., and let 6(B) be the set of sentences deduced by the belief subsystem from a base set B. We say that 6 is decidable if 6(B) is decidable for all B. An extension of 6 is a subsystem whose deduction rules are a superset of R.. Now suppose 6 is decidable, and consider the following questions:

1. Is there an extension 6 1 of 6 such that, for all base sets B and all sentences a,
2. if a E 6'(B), then [S]a E 6'(B), and
3. if a ~6'(B), then ~ (S]a E 6'(B) 7
4. Is 6 1 decidable7
5. Is the theory of 6' decidableT

\Ve haYe proven the following about these questions. In general , (1) must be answered negatively, as not all subsystems are extendable. There are specific types of subsystems for which extensions satisfying (I) exist, however (e .g., if the base set contains no instances of the self-belief operator ). 2 If an extension exists, it is decidable. But the theory of a decidable extension is not , in general, decidable; there exist counter­ examples to (3). 3

Even though a complete, decidable implementation of the Recursion Property does not exist in all cases, we can find incomplete approximations. The idea is that the undecidability results from the unboundedness of belief recursion, that is, reasoning about an agent reasoning about an agent . .. , in an unbounded manner. Suppose, however, we place a bound on the depth of such reasoning: as the deductions involve higher embeddings of belief subsystems, the rules become weaker, and eventually the line of reasoning is cut off at some finite depth. Belief subsystems satisfying this property are said to have Bounded Recursion. Bounded Recursion subsystems are a nice example of resource limitations in belief deduction.

2 The work or Levesque (2) is helprul in finding classes of extendable systems.

3 The proor or this uses Kripke's well·known result that monadic SS is

undecidable.

3. A Propositional Deductive Belief Logic

We present a logic, B, for Deductive Belief. For simplicity and ease of comparison with other modal systems, we assume a (modal) propositional internal language. The logic is capable of representing belief subsystems with or without the Bounded Recursion property. It is sound and complete with respect to these models.

3.1 Sequent Systems and Views

The general model of deduction that we aSsume is a block tableau sequent system. Block tableaux have much in common with PLANNER-type theorem-provers, and also have nice formal properties; the interested reader is referred to Smullyan [5]. The treatment here will be necessarily brief.

Let S; be a set of (names for) agents, and let L be a modal propositional language, with unary modalities (S;) ([S;)a means "agent S; believes a").. Let capital Greek letters stand for finite sets of sentences of L (lower Greek letters stand for single sentences). A sequent is an ordered pair of sets written as f=t~ , and read as ·~ follows from r :" A sequent f=t~ is true in a Boolean valuation iii the sentence (11 "12"· .. )=> (61 v62v .. . ) is true.

A block tableau system T consists of a set of axioms and deduction rules. A sentence a is a theorem of a system T if there is a closed block tableau whose root is the sequent =ta. A set of sentences r is inconsistent if there is a closed tableau for f=t. We make use of a set of rules To that are propositionally complete, i.e., all tautological consequences can be derived using To (see Smullyan [5]).

Although we have given a semantic treatment of sequents above, they have a natural interpretation in terms of derivability, and it is this interpretation we exploit to formalize belief subsystems. Consider the belief subsystem of agent S;. This subsystem has a set of effectively computable deduction rules, represented as a block tableau system; call the set of rules r(i). Suppose f=t;a is a theorem of this system (we use a subscript on the sequent sign to denote that this sequent refers to S;'s belief subsystem). If all off are beliefs of S;, then, by the Closure Property, a must be also, since a is deducible from r , according to S;.

For any view v, we can thus characterize the belief subsystem by a set of tableau rules r(v). These, together with t ableau rules that relate sentences in one view to another, constitute the system B , which we give below (the following abbreviation is used: (S]f =dr (SbJ. (8]12, . . . ).

• The propositional rules To .
• Rules r(v) for each view v.

Remarks. There are three parts to the theory B . The first part is a set of rules formalizing the outside observer's Boolean system. These rules incorporate the nonsubscripted sequent sign ( =t ). A propositionally complete deductive system is employed here (i.e., To), since we are interested in deducing all we can concerning the belief systems of the agents. Properties of belief systems in general are always stated using the observer's sequent; for example, to show formally that, if any agent believes p, he believes he believes p, we prove that the sequent [S;)p=t[S;J[S;)p is a theorem of B. The second part is a set of rules formalizing the propositional component of each view (=tv). These rules involve the sequent sign ,..v, since they talk about agents' deductive systems.

The third part of B formalizes the constructive component of the Deductive Belief model, characterizing the way in which the outside observer views agents' deductive systems, and the way in which agents view their own and other agents' systems. In general these rules have intermixed occurrences of sequent signs with different view indic.es. Rule Cut· implements the Closure Property for each view, by saying that, if fJ follows from believing n, and Q from fJ (and possibly additional beliefs r), then {J follows from believing n (and r). Rule Bs formalizes the deductive system of an agent from the point of view of an outside observer and other agents. The key part to this rule is that the modal operators get dropped from (S;)r and one of [S;)~ in going from the top to the bottom sequent. This part of the rule can be informally read as, "in any view, S; believing 6 follows from his believing r if, in that view of S;'s deductive system, 6 follows from r." When put this way, rule Br, is simply a formal statement of the basic concept of deductive belief given in the last section.

There are two other interesting components to B6 : both [S;)~ and [S;)r get repeated on the bottom sequent. The reason for this is to capture the introspective properties of belief; namely, if an agent believes r , then he believes that he believes it, and if an agent doesn't believe ~. then he believes that he doesn't believe it. Note that Bs is appropriate only if agents actually have complete knowledge of their own beliefs. As we indicated in the last section, this is not always even theoretically possible. In this case, weaker versions of Br, must be used. If an agent doesn't know all the things he doesn't believe, then (S;)~ is dropped from the bottom sequent. If he doesn't know all the things he does believe, then (Si]r is dropped.

Finally, we need a separate rule to state a consistency condition on beliefs, if this is desired.

This rule states that S; believing r is logically inconsistent, if r is-ueductively inconsistent in S;'s deductive system (recall that n=t; means that the n are logically inconsistent).

· We have proven the system B to be both sound and complete with respect to the Deductive Belief model.

3.2 Comparison to Other Modal Systems

Most AI research on formal representations of belief and knowledge is based on Hintikka's adaptation of Kripke's possible-worlds model (e.g., (4], [3)). Possible-worlds models, by their very nature, require that all logical consequences of an agent's beliefs are also beliefs; a possible-worlds model cannot take into account resource limitations that might be present in an agent's belief system. The propositional modal logic that formalizes the possible-worlds model of belief is weak SS, that is, SS without the condition that all beliefs are true. We have proven that B reduces to this system under the following conditions:

1. The propositional rules r(v) lor each view v are complete, and
2. Belief recursion is unbounded.

In addition, if a modified form of Br. is used in which an agent doesn't know everything he doesn't believe, then under the same conditions B reduces to weak S4. Thus, under the assumption of deductive completeness and an infinite resource bound, the B reduces to more familiar belief logics.

4. Conclusion

We have introduced the concept of robot belief subsystems parameterized by a finite set of base sentences and a set of deduction rules. This Deductive Belief model is a viable alternative to possible-worlds models of belief and has the attractive property of taking resource limitations into account in deriving consequences of beliefs. We have formalized the Deductive Belief model for the propositional case with the logic B, which is sound and complete with respect to our model.