A New Logic of Beliefs: Monotonic and Non-Monotonic Beliefs - Part 1

1. Introduction

The fundamental assumption in this paper is that the dis­ tinction between the notion of truth of the belief of a propo­ sition P and that of P lies in the underlying contexts of worlds. In the case of beliefs, the context is a set of worlds whereas in the case of propositions the context is a single world. We say that Pis believed by an agent in the context W, which is a set of worlds, if Pis true in every world wi E W. Put another way, the agent believes in any thing unless there is evidence to the contrary. Why does the context being a set of worlds make a significant difference? First, the meaning of negation as in B..,P is now different from the meaning of negation as in -BP. 1 By B-J> = "believe in negation of P", we mean that Pis false in each wi E W, which is quite different from -BP, meaning that P is false for at least one wi E W. Thus, B-,P :F. -BP. Second, it is possible that an agent believes neither P nor -J>. It is also possible that he believes both P and -J> simultaneously, i.e., assert BP 1\ B-,P, which can happen only in the extreme case W = 0. Note that every thing is believed when W = 0, including the propositional false-formula, denoted by D.

1 We use "-" for negations applied to beliefs, to distinguish it from the negation"-," applied to propositional formulas.

In defining a logic for beliefs, one of the first ques­ tions that arises is what is its relationship to the standard logic. For example, if cj>1 and c1>z are two equivalent propo­ sitional formulas, then is Bc!> 1 considered to be equivalent to Bc!>z? More generally, if 411 is believed and 411 logically implies 412, then should 412 be also believed? Note that if the answer to the second question is 'yes', then the same is true for the first question. For the belief-logic defined here, both the answers are 'yes'. A different belief-logic is defined in [Levesque, 1984] specifically to allow Bcj>1 not to be equivalent to B41 2 even though cj> 1 and 41 2 may be equivalent as propositional formulas. This is achieved by considering a general notion of a world wi in which the truth value of a proposition P may be true (T), false (F), undefined, or simultaneously true and false (i.e., P does not have a unique truth value). These general worlds are used for modeling the "explicit" beliefs whereas the "implicit" beliefs are modeled (for the most part) by the standard worlds, with each proposition having a unique truth value.

For the logic of belief described here, only the stan­ dard worlds are considered. We do not distinguish thus the explicit beliefs from the implicit beliefs. More importantly, we consider each propositional formula c1> as a special kind of belief-formula cj>' whose truth value is evaluated in the same way as that of the general belief-formulas. This is not the case in [Levesque, 1984]. Another interesting property of the belief-logic given here is that one can apply the con­ struction repeatedly to obtain a hierarchy of belief-logics BLk, k ~ 1, where BLk can handle formulas involving up to level k nested applications of the belief-operator B. Thus, the formula B(41' v B'l')-note the use 41' instead of c1> - can be handled in BL2· The belief-logic in [Levesque, 1984] can consider such nested formulas directly. How­ ever, we feel that our formulation of belief-logic is actually more natural in that it explicitly recognizes the inherent higher complexity of the formulas with higher nested levels of B and handles them in a higher level (larger value of k) logic BLk.

We give here a simple inference technique for the new belief-logic (= BL1) by generalizing the resolution method in propositional logic. A similar generalization of the resolution rules for BLk-t immediately gives the reso­ lution rules for BLk, k ~ 2. In Part-I, we present only the basic monotonic form of the belief-logic BL1· The con­ struction of a non-monotonic form of BL 1 (and other BLk, k > 1) by using the circumscription is presented elsewhere [Kundu, 1991b]. Note that the separation of the non­ monotonic aspects from the monotonic aspects of beliefs makes it easier to model a world and control the inferenc­ ing in it

2. Basic Notions

We formally define a formula of the form Bcjl, where cjl is a propositional formula, to be an atomic belief-formula. A general beliefjormula is defined to be an atomic belief­ formula or a formula which is obtained by logical combina­ tion of other belief-formulas via"· v, and-. We use"~" as an abbreviation for the usual logical combination of v and---, (or-). Thus, -B---,P v B(P ~ Q) is a belief-formula, but BB-.P is not Note that the operator B is considered to have higher precedence than"· v, and~.

Let { P 1> P 2, ··· , P 11 } be the basic propositions in our universe of discourse. We denote by 0 11 the set of 2 11 indi­ vidual worlds defined by the combination of.T/F values of the Pi 's. For W ~ 0, we say Bcjl has the truth value T at W if cjl is true at each wi e W. In that case, the set W is said to be a model of Bcjl. The truth value of a complex belief­ formula is defined in the usual way by combining the truth values of its subformulas via the connectives {A, v, ---,,and ~}. In particular, -Bcjl is true at W if and only if cjl is false at at least one world wi e W. Clearly, the only model of BO is the empty subset 0 !:: 0 and the models of -BO are all non-empty subsets of 0. On the other hand, the models of Bcjl" -BD are the set of all non-empty models of Bcjl, i.e, the non-empty subsets of the set of models of cjl; the only model of Bcjl" B-.cjl is W = 0. We write O(p) for the set of models of a belief-formula p and write O(cjl) also for the set of models of a propositional formula cjl. By abuse of notation, we let 0 denote also the false belief-formula, which should not cause any confusion; similarly, we write T = -0. The belief-formula p is said to be a tautology or valid if O(p) = 2°. It is easy to see that Bcjl is valid if and only if cjl is a valid propositional formula. The notion of satisfiability of a set of belief-formulas and its models are defined in the usual way.

We say a belief-formula P1 is equivalent to another belief-formula P2 if they have the same models, in which case we write P1 = p2· Table 1 shows some simple equivalences of belief-formulas. Note that BO :1:- 0 and, in general, Bcjl1 v Bcjl2 :1:- B(cjl1 v cjlz}.

We say P1 implies P2 or P2 can be inferred from P1· if P1 ~ P2 is valid. In symbols, we write P1 => P2· It is clear that Bcjl 1 v Bcjl 2 implies B(cjl 1 v cjlz), but as we noted above the converse may not be true. One can derive [B$1 v Bcjlz] => B[cjl 1 v cjlzl by repeated application of Theorem 1 below. First, since cjl 1 => cjl1 v cjl2, we get Bcjl1 => B[cjlt v cjlzl and, similarly, Bcjl 2 => B[cjl 1 v cjlz). In propositional logic, we also have cjl1 =>'I' and $2 =>'I' implies [cjl1 v cjlzl =>'I'· The same is true if cjl1, cjl2, and 'I' are replaced by arbitrary belief-formulas. By putting Bcjl 1 in place of cjl 1 , Bcjl 2 in place of cjl2, and B[cjl1 v cjlzl in place of 'I'· we get that Bcjl1 v Bcjl2 => B[cjl1 v cjlzl. The following Modus-ponens for belief­ formulas is also immediate from the definitions.

If P1 and P1 ~ P2 are valid belief-formulas, then P2 is a valid belief-formula.

Theorem 1. For any two propositional formulas cjl1 and q, 2 , we have

1. cjl1 => cjl2 if and only if Bcjl1 => Bcjl2 if and only if -B$2 => -Bcjlt.
2. -B(cjl1 v cjlz} => -B($1)" -B(cjlz}.
3. B(---,cjl1) "-BO => -B$1·

Proof. Immediate from the definitions. ·

The following theorem shows that belief formulas are sufficiently powerful to describe any family K of sub­ sets of 0, i.e., K ~ 2°. In particular, if N = 101 = 2 11 , then the number of distinct (non-equivalent) belief-formulas over the propositions {P 1 , P 2 , ... , P 11 } is 2t' whereas the number of distinct propositional formulas is only i'.

Theorem 2. If K is an arbitr2.1)' family of subsets of 0, then there is a belief-formula PK whose set of models equals K, i.e., O(PK) = K. Moreover, P is unique up to equivalence.

Proof. If K = 0, then we take PK =D. Now let K = (W 1 , W2, ... , W 171 } . We first show that there is a beliefformula ~w which has a unique model W for any W ~ n. If W = 0, then ~w = BO. Now assume that W -:~; 0. For each world w; e W = (w1, w2, ... , wq}, let C; be the conjunction of the form Z 1 " Z2 " ... " Z,., where each Z; = P; or -.P;, such that the propositional formula C; has exactly one model W;. The belief-formula ~w = B(C1 v c2 v ... v Cq) "-B-,C 1 "-B-,C 2A ... "-B-,Cq then has the unique model W. If we write ~i for the formula whose unique model is W; e K, then ~K = ~1 v ~2 v ... v ~ ... satisfies the theorem. The uniqueness of ~K is immediate. ·

The belief-formula ~K obtained in the proof of Theorem 2 may be called the disjunctive normal form of a belief-formula whose models are K = (Wlt W2, ... , W,.}. Example 1 shows some families of subsets of ~ and the associated disjunctive normal form belief-formulas. The proof of Theorem 2 suggests the notation Ncj) = -B-,C 1 " -B-C2 " ... "-B-,Cq, where 4> = C 1 v C2 v ... v Cq is a disjunctive normal form propositional formula. The for­ mula Ncj), which may be read as "necessarily contains (or implied by) cj)", has the models (W: Q(cj))!::: W}. In partic­ ular, the models of NO is 2° and thus NO= T.

Example 1. Consider the universe of discourse con­ sisting of two proposition (P 1, P 2}. Thus Q = ( w 0 , w 1 , w2, w 3}, where w0 corresponds toP 1 = F = P 2, w 1 corresponds toP 1 = F and P 2 = T, etc. Table 2 shows some of the fami­ lies K !::: 2° and their associated disjunctive normal form belief-formulas ~K. Here, we write P 1 " P 2 in short as P 1P 2,-.P1AP2as-.P1P2,etc .·

In view of Theorem 2, we can associate a belief­ formula cj)' with each propositional formula 4> in an one-to­ one fashion such that the set of models of cj)' is given by Q(cj)') = ( (w; }: w; e Q(cj))}. In particular, 0' = 0 though T' -:~; T. The mapping from 4> to cj)' is consistent with the logical operations " and v in the sense that

In general, (-,cj))' -:~; -(cj)'), which should not be surprising since B(-,cj))-:~; -Bcj). Nevertheless, if 4>1 and 4>2 are two pro­ positional formulas and 4>1 ~ 4>2, i.e., -,cj)1 v 4>2 is a tautol­ ogy in propositional logic, then we have 4>1' ~ 4>2' for the associated belief formulas, i.e., -(4>1 ') v ~,is a tautology in belief-logic. The following theorem, where 4> may also be 0 or a tautology, is immediate and is illustrated in Table 3.

Theorem 3. For any propositional formulas 4>1 and 4>2, we have 4>1' ~ Bcj)1 and B-,cj)1 ~ -(4>1 '). Also, «1>1 ~ «1>2 if and only if 4>1' ~ «1>2'. ·

3. Resolution Method for Beliefs

The inference problem in a belief-logic consists of deter­ mining whether a given goal belief-formula ~0 is implied by a finite set of belief-formulas S = (~lt P2 .... ~t}, called facts. We present a resolution method for inferencing in the belief-logic, which is a generalization of the resolution method for the propositional logic. The derivation of 0 in the belief-logic often involves as a substep the ~erivation of BO, ~eaning that the facts which are believed are contrad­ ictory to each other (as in Bel> and B-,cj)). The final deriva­ tion of 0 shows that the beliefs themselves are in contrad­ iction with each other (as in Bcj) and -Bcj)).

We begin by defining the notion of literals, clauses, and the resolvent If Cis a propositional-clause, including the case C = 0, then BC and -BC are said to be belief literals; BC is said to be a positive literal and-BC a nega­ tive literal. A belief-clause is a disjunction of zero or more belief-literals. We sometimes use the term "literal" as a short form of "belief-literal" and also of "propositional­ literal", when no confusion is likely; similarly, the term "clause" is used for both "belief-clause" and "propositional-clause". It is clear from Table 1 that each belief-formula is equivalent to a conjunction of belief­ clauses.

We define the notion of subsumption between two belief-clauses ~1 and ~2 in such a way that the following holds: If ~1 subsumes ~2· then each model of ~1 is a model of ~2· i.e., ~1 ~ ~2 is valid. This means, in particular, that we can remove a clause ~ i from a set S if it is subsumed by some other clause in S without affecting the satisfiability or unsatisfiability of S. Formally, we define the subsumption as follows:

1. If e 1 and e 2 are two propositional clauses such that e 1 subsumes e 2, then we say Be 1 subsumes Be2 and -Be2 subsumes -Be1· (It is not possible for a positive belief-literal Be 1 to subsume a negative belief-literal -Be2 because 0 e Q(Be1) - Q(-Bez). The only case where a negative belief-literal subsumes a positive belief-literal is -BT = 0 subsuming Be 2, e 2 being arbitrary, and -BC 1 subsuming BT = T.)
2. More generally, a belief-clause ~1 is said to subsume another belief-clause ~2 if each literal in ~1 equals or subsumes some literal in ~2. The empty belief-clause 0, which has no literals in it, subsumes all other belief­ clauses.

Thus, -BP~ v BP2 is subsumed by -BP1; also, -BP1 is subsumed by -B(P 1 v Pz) or, more generally, by a clause of the form

We first define two types of resolvents for belief­ literals, called Type-I and Type-II. These are then general­ ized to the case of arbitrary belief-clauses. Finally, we define a third type of resolvents, called Type-III. One can actually generalize the other two resolvents to include the Type-III resolvent, but we choose to formulate it separately for the sake of clarity. In each. case, we make sure that the resolvent is logically implied by the parent clauses from which it is derived.

• (1 °) Type-/ resolvent.

If Be 1 and Be 2 are two belief-literals such that e 1 and e 2 are propositionally resolvable, then we say that Be 1 and Be 2 are resolvable and we define their resolvent to be the literal given by (R.l).

Thus, we have res(B(P v -,Q), B(Q v R)) = B(P v R). It is clear that Be1 "Be2 ~ B(res(eh ez)). Note that this type of resolvent can be at best BO, but notO.

• (2°) Type-// resolvent. Let e 1 = L 1 v L2 v ... v L,. and e 2 = Lk+1 v Lk+2 v ... v L,. v e 1 2 be two propositional clauses, where 0

::;; k < m and each L i is a propositional literal; e 1 2 may be the empty clause. Then, we say that Be 1 and -Be 2 are resolvable and we define their resolvent to be the clause given by (R.2).

Two special cases of (R.2) that are worth noting are: res(BO, -Be z) = 0 = res(Be 2, -Be z), and res(Be 1o -BD) = -B(-,L1) v -B(-,Lz) v ... v -B(-,L,.). Once again, we have Be 1 "-Be 2 ~ res(Be 1, -Be z).

• (3°) Generalization of (R.1) and (R.2). Two belief-clauses ~1 =X 1 v X 2 v ... v X,. and ~2 = Y 1 v Y 2 v ... v Y,. are said to be resolvable if there is a literal in ~1 (say, X,.) which can be resolved with a literal in ~2 (say, Y 1) using (R.1) or (R.2). We define the resolvent res(~1 · ~ to be the clause given by (R.3) below. We say (R.3) is of Type-I or Type-11 according as res(X,., Y 1) is of Type-I or Type-II. Note that ~1 and ~2 may contain several pairs of literals with respect to which we can form res(~1 · ~z) and we may obtain different resolvents in this way. (This is unlike the case of propositional logic, where one obtains a unique resolvent no matter how it is resolved.)

If the right hand side of (R.3) contains duplicate literals, i.e., Xi = Yi for some i::;; m-1 and j ~ 2, or res(X,., Y 1 ) equals some of the other literals, then we simplify it by removing the duplicate literals. That ~1 " ~ ~ res(~1 · ~z) follows from the corresponding properties of (R.1) and (R.2).

• (4°) Type-III resolvent. Let~= X 1 v X2 v ... v X,., m ~ 2, where each Xi= -B(C v ei) is a negative literal and Cis the largest common subclause of the propositional clauses { C v ei: 1 ::;; j ::;; m}, i.e., there is no literal common to all ei. Then ~ is subsumed by -BC and we define the resolvent res(~) to be the literal given by (R.4).

A derivation of a belief-clause ~ from a set S of belief-clauses is defined to be a sequence D = (D 1, D 2, ... , D,.), where each Dk e S or is a resolvent of some previous clause(s) in the sequenceD and D,. = ~· A refutation proof of a goal ~0 from a set of facts {~1> ~2 .... , ~k} is a derivation of D from the union of the sets of clauses obtained from ~ i , 1 ~ j ~ k, and the clauses obtained from ---,~0. There is no restriction on how the clauses of ~ i and of -~0 are formed.

Example 2. Shown below are the minimal unsatisfiable sets of clauses S in a single proposition P, which do not contain D. 2

1. BD and one of (-BP, -B-.P, -BD}
2. (-BP,BP}
3. (-B-.P, B--J>}
4. (BP, -BD, B--J>}
5. ( -BP v BD, BP v B-.P, -B-.P v BD, -BD}

It is easy to see that D can be derived in each case. There are three ways of deriving D in case (4). One of the many possible ways of deriving D in case (5) is shown in Fig. 1. If we replace one or more of the input clauses by their alternate representations (e.g., replace -BP v BD by -BP v B-.P), then one can still derive D. ·

Example 3. Suppose our universe of discourse con­ sists of the basic propositions P = "Tweety has wings" and Q = "Tweety flies". Let B be the belief operator "Kundu believes ... ". We consider the following facts (1)-(2) and the goal (3):

1. "Kundu believes that if Tweety has wings, then Tweety flies". This is represented by B(P--+ Q) = B(...,P v Q).
2. "Kundu does not believe that Tweety does not have wings". This is represented by -B--J>.

2 The minimality of S means that S does not contain a proper subset which is also unsatisfiable. In particular, no clause inS is subsumed by another clause inS.

(3) "Kundu does not believe that Tweety cannot fly". This is represented by -B-.Q.

One expects that perhaps (3) can be proved from (1)-(2). Fig. 2 shows a refutation proof of (3). If we replace (2) by the stronger fact BP" -BD, then we can indeed still prove the goal (3). We first resolve BP with B(-,P v Q), giving the resolvent BQ. Now, obtain BD = res(BQ, B-,Q), which can be then resolved with -BD to obtain the desired empty-clause D. Note the use of -BD here, without which we cannot obtain D in this case. This is not surprising because the empty set of worlds 0 is a model for (BP, B(P--+ Q), B-.Q}. We can actually derive a stronger goal BQ " -BD in this case.

""'/

Figure 2. An illustration of resolution proof for beliefs.

If we consider the goal (3') = BQ = "Kundu believes that Tweety flies", which is stronger than (3), then it may not be so obvious if (3') can be proved from (1)-(2). Fig. 3 shows all possible resolvents that can be obtained from ( (1 ), (2), -(3')} and, in particular, that D cannot be derived. The set of worlds W = (TI, FF}. where TI means P = T = Q and similarly for FF, forms a model of ( (1), (2), -(3')}.

·

The main result of this paper is the following theorem. We omit the proof for want of space, but it can be found in [Kundu, 1991a]. We point out that the resolution rules given here can be seen to be closely related to that for predicate logic (without function symbols). One could almost say that the completeness of the belief-logic infer­ ence method follows from that of predicate logic without function symbols, except for the slight difference of the empty set of worlds being a possible model for a given belief-formulas.

Theorem 4 (Completeness and soundness of the resolution method). Let S be an arbitrary finite set of belief-clauses. The setS is unsatisfiable if and only if there is a derivation of 0 from S. ·

4. Conclusion

We have presented here a new belief-logic for proposi­ tional facts (i.e., without variables and quantifiers), includ­ ing a resolution proof method for this logic, which can be thought of as a generalization of the resolution method for propositional logic. Our fonnulation of the belief-logic differs from the other belief-logics in two fundamental ways: (1) The ordinary propositional logic is imbedded within our belief-logic. Each propositional formula cp is mapped to a belief-formula cp' in an one-to-one to fashion in such a way that if cp implies 'I' as propositional formulas, then cp' implies 'I" as belief-formulas, and conversely. Also, the truth value of cp' is evaluated in the same way as for general belief-formulas. (2) The belief-logic developed here is monotonic in nature and its construction can be applied repeatedly to obtain a hierarchy of belief-logics BL1r.o k;;::: 1, such that BLk :::> BLk-t and BLk can handle all belief-formulas involving up to level k nested applica­ tions of the belief-operator B. We obtain a non-monotonic belief-logic from BLk by applying circumscription to it, for instance. This is the approach taken in [Kundu, 1991 b].

• Acknowledgements: The author wishes to express sincere thanks to an anonymous referee for indicating the close connection between the resolution rules given here and those of predicate logic.
• Appendix: Consider the universe 0 = {w0, wtl of a single proposition P. Shown below are all the belief-literals and their models. There are only three belief-clauses which are not equivalent to a belief-literal or T, namely, -BP v BD = -BP v B--J>, -B--J> v BD = -B--J> v BP, and BP v B--J>. The set of models for these clauses are given by {0, {w0}, {w0, wtl}, {0, {wtl. {w0, wtl }, and {0, {w0}, {wtl}, respectively.

The following diagram shows the subsurription relation­ ships among the belief-clauses other than T, where a clause ~1 is shown below another clause ~2 if ~1 subsumes ~2·

References:

• [Anderson and Belnap, 1975] A. R. Anderson and N.D. Belnap. Entailment, the logic of relevance and necessity, Princeton University Press, 1975.
• [Hintikka, 1962] J. Hintikka. Knowledge and belief: An introduction to the logic of the two notion, Cornell University Press, 1962.
• [Levesque, 1990] H. J. Levesque. All I know: a study in autoepistemic logic, Artificial Intelligence, 42(1990), pp. 263-309.
• [Levesque, 1984] H. J. Levesque. A logic of implicit and explicit belief, Proceedings of National Confer­ ence on Artificial Intelligence, AAAJ-84, Aug. 6-10, 1984, pp. 198-202.
• [Kundu, 1991a] S. Kundu. A new logic of beliefs: monotonic and non-monotonic beliefs -Part I, Tech Rept., 91-003, Louisiana State University, Computer Sc. Dept, 1991.
• [Kundu, 1991b] S. Kundu. A new logic of beliefs: monotonic and non-monotonic beliefs - Part II, in preparation.