Non-Omniscient Belief as Context-Based Resoning

1 The approach

This paper describes a general framework for the formal­ ization of monotonic reasoning about belief in a multia­ gent environment . The most common solution is to take a first order (propositional) theory, to extend it ~sing a set of modal operators, { Bi }iEI, and to take B' A as meaning that an agent ai believes A (see for instance [Halpern and Moses, 1985]). There is only one theory of the world, however this theory proves facts about the agents' beliefs. According to a first interpretation, this theory is taken to model things how they really are. It is therefore a finite (and possibly incomplete) prese~tation of what is true in the world, and the fact that B' A is a theorem means that it is, in fact, the case that ai believes A. According to another interpretation, this theory is taken to be the perspective that a generic reasoner has of the world. It is therefore a finite presentation of the reasoner's beliefs, and the fact that Bi A is a theorem means that the reasoner believes that ai believes A.

Once one accepts the second interpretation (as we do), a mechanized theory is naturally take.n ?B .repre­ senting the beliefs of the computer where 1t 1s Imple­ mented. Moreover, in the case of multiagent belief, a further step is to have, together with the theory of the computer, one theory (at least, see later) for each agent .

· Alessandro Cimatti a.nd Kurt Konolige ha.ve provided very useful feedback a.nd suggestions. The work a.t IRST has been done as part of the MAlA project. This paper is a short version of the IRST technical report #9206-03 .

The theory of the computer plays the same role as the unique theory in the modal logics approach. The agents' theories are the (mental) representations that the com­ puter has of the agents themselves. The computer has beliefs about the beliefs of the agents not because, as it happens in the single theory approaches, it "simu­ lates" them in its own theory but, rather, because it can infer, say, Bi("A") from the fact that A is a the­ orem in the ai 's theory. (In this framework, theories are called "contexts" and the formal systems, which are basically defined as sets of contexts, are called mul­ ticontext systems (MC systems) and, sometimes, mul­ tilanguage systems (ML systems) [Giunchiglia, 1991; Giunchiglia, 1993].)

All the previous work on the formalization of proposi­ tional attitudes, namely modal logics and the syntac­ tic approach (where belief is a first order predicate, see for instance [Konolige, 1982]) makes use of a sin­ gle theory. However, ideas similar to ours, which sug­ gest the use of multiple distinct theories, have been ex­ ploited in much applied work in computational linguis­ tics and AI (see for instance [Wilks and Biem, 1979; Giunchiglia and Weyhrauch, 1988]) . There are in fact many implementational advantages, all deriving from the fact that reasoning becomes intrinsically localized [Giunchiglia, 1993] (for instance: the modularization of the knowledge base, computational efficiency - due to the division of the search space in smaller search spaces - and the possibility of parallelization of the reasoning process). Our formalism seems quite close, arguably closer than the previous approaches, to the current prac­ tice in the more applied implementational work. In­ deed this is one of the main motivations . underlying our work and MC systems have been implemented inside the GETFOL system, [Giunchiglia, 1992] an extension of are­ implementation of the FOL system [Weyhrauch, 1~80] . However in this paper we focus on the representatiOnal issues and argue that our approach allows for more natu­ ral and more intuitive formalizations (see also [Dinsmore, 1991]).

In [Giunchiglia and Serafini, 1991] we have described and motivated the basic system, which models logically omniscient agents. In this paper we take a step fur­ ther and treat the problem of non saturated· belief, that is the fact that real agents never believe all the logi­ cal consequences of their basic beliefs . Our treatment is based on a distinction between ideal and real reason­ ers. We show how ideal and (different) real reasoners. can be modeled by contexts with different structural proper­ ties (section 2) and/or different connections among them (section 3). Our approach presents various advantages. First, it allows for an exhaustive classification of all the basic forms of non logical omniscience (see sections 2, 3). Second, all the various forms of non logical omniscience can be identified as a distinct structural property of the system. Third, complex forms of non logical omniscience can be "constructed" by composing simpler forms into the structure provided by the system for saturated belief (see sections 2, 3). All the cases studied in the past plus new interesting ones are captured by this classification (see section 4). Fourth, deductions can be performed very naturally by exploiting the fact that each reasoner is modeled as a distinct theory (section 5) 1 .

2 Ideal and real reasoners

As informally described in the previous section, reason­ ers (e.g. agents and the computer itself) are modeled as logical theories, which we present as axiomatic for­ mal systems. Technically, we define a formal system E as a pair consisting of a language LE and a set of the­ orems TE<;LE, i.e. E = (LE, TE)· LE is defined as the smallest set generated from the set of propositional letters (atomic formulas) ~ and closed (by C) under the set of formula building operations WE, in formulas LE = C(~, WE)· Analogously, TE is defined as the smallest set generated from the set of axioms OE and closed under the set of inference rules ~E. in formulas TE = C(OE, ~E)· OE is also called the set of the basic beliefs.

A first approach is to take a reasoner I = (LI, TI), such that, given a set PI of atomic formulas and a set 0 1<;LI of true facts, it believes all the tautologies and logical consequences of OI . OI is therefore l's set of ba­ sic beliefs. Technically, this implies that WI and ~I are complete for a propositional language and for proposi­ tional logic, respectively. In this case we say that I is an ideal, logically omniscient reasoner.

The problem is that real reasoners are not logically omniscient. Given them enough knowledge and re­ sources (e.g. space, time), real reasoners tend to con­ verge to the behaviour of an idealized reasoner but this may never be the case. Thus, if we take E = (LE, TE) to be a reasoner which is the "realized" version of I, a plausible model for E is that LE<;Lr and TE<;TI. This captures the intuition that the ideal reasoner is the limit saturated case of the real reasoner in the sense that E's beliefs are always a subset of I's beliefs. However it is possible to ask for stronger notions of realization . For instance, if l-1: is the consequence relation of E (that is the set of pairs (r, A), with r U {A} E LE, such that there exists a derivation of A from f), we could impose that 1-E <; 1-1. Intuitively this means that not only do we ask that E's beliefs are a subset of l's but also that E's ability to compute the logical consequences of sets of assumptions is weaker than I's. In the following we consider the case TE<;TI.

1 For lack ofspa.ce, these ideas are described only partially. For instance, we state theorems but we do not prove them. We do not consider nested belief. We do not give semantics ([Giunchiglia et al., 1992] presents a somewhat old semantics for the basic saturated case). We do not give any complexity argument; although it is intuitive that reasoning with con­ texts saves time; we have not done any in depth analysis on this issue.

The recursive definition of LE and TE allows for an exhaustive classification of all the possible ways for a reasoner to be not ideal. We may have LE C LI and TE C TI because E's basic sets (PE, OE) or because E's constructors (WE for formulas, ~E for derivations and theorems) are "incomplete". Technically, this intuitive notion of incompleteness can be made precise as follows .

Definition 2.1 Let S1 = C(B1, Fl), S2 = C(B2,F2) be two sets such that S1 C S2 . We say that

• B1 is incomplete wrt B2, and write B1 --( B2, iff C(B1, FI) C C(B2, F1). We also say that S1 is in­ complete (wrt S2) in the basic facts .
• F1 is incomplete wrt F2, and write F1 --( F2 , iff C(B1,F1) C C(B1,F2). We also say that S1 is in­ complete (wrt S2) in the construction rules.

"~" is defined in the obvious way. Set equality, written "=", is the equivalence relation for ~- LE and TE may be incomplete (wrt LI and Tr respectively) because of their basic facts or because of their construction rules (or both). This suggests the classification below. Let us start from the incompleteness in the language.

Incompleteness in the signature (PE --( PI). In this case we take PE --( Pr to mean PE C Pr, namely that E is not aware of some primitive propositions (we sup­ pose that real reasoners know the logical connectives) . As pointed out in [Fagin and Halpern, 1988], supposing that P is the proposition expressing that personal com­ puter prices are going down, it is very likely that a Bantu tribeman is not aware of P.

Incompleteness in the formation rules (WE --( Wr ). E is aware of a set of propositions. Still he does not succeed in composing some complex propositions . This may happen for two reasons. In the first case, similarly to the case of incompleteness in the signature, E simply does not know some formation rules (WE C WI). For instance even if it knows the logical connective for con­ junction, he does not know how to build P1/\ P2 from P1 and P2 . In the second case E suffers from a form of lim­ itation of resources and it is not able to form sentences beyond a certain level of completeness, e.g. longer than a certain limit. For instance a sentence with one hundred constants rises problems of space and time. Notice that in this case (WE ct. WI).

A similar classification can be given for TE .

Incompleteness in the axioms (OE --(Or) . This means C(OE, ~E) C C(Or, ~E) · A first possibility is that OE c OI . This may have two causes. The first is due to the fact that incompleteness in the signature or in the formation rules may imply OE c OI (as OE<;LE) · However, and this is the second case, we may think of situations where E is aware of a proposition but without knowing whether, it holds. Technically these two situ­ ations are distinguished as in the second case we have C(flE, .6.E) C C(flr n LE, .6.£). The second possibil­ ity is that nE ¢.. flr. Technically this situation is easy to construct. It is sufficient to substitute some axioiilB with some new "weaker" ones which are not contained in 01 . The issue here is whether an E so defined can still be considered the realized version of I. Intuitively one would like to have an operation of realization which amounts to limiting the capabilities of the ideal reasoner without "creating" anything really new. However con­ sider the situation where I believes A and A :::> B and E believes B. In this case it seems plausible to say that E is a realization of I.

Incompleteness in the deduction rules (.6.E -< .6.r ). This case Is entirely dual to that for WE. That is, we may have ignorance of some rules (.6.E C .6.1 ) or resource bounded ness (.6.E ¢.. .6.r ).

3 MC systems for belief

In this paper we take the computer to be logically om­ niscient. Even under this hypothesis, we are able to build systems whose provability relations are equivalent to those of all the systems defined in the past.

3.1 Saturated belief

We start by considering the case with an agent which is the ideal reasoner I described above. We have two contexts, one for I and one for the computer c having beliefs about l's beliefs. We take IB to be the belief predicate for I in Lc. For IB to mean (in c) belief of I we require that the following two properties hold:

• c must be complete for I: for any wff A believed by /, IB("A") is believed by c.
• c must be correct for /: for any wff of the form IB( "A") believed by c, A is believed by I.

Technically, these properties are obtained via certain bridge rules (i.e. rules whose premises and conclusions belong to distinct contexts) which allow us to prove IB( "A") in c just because A is a belief of I and, vicev­ ersa, to prove A in I just because IB( "A") is a belief in c. Figure 1 gives a structural description of the resulting system, called MBI. MBI is defined as follows (MC sys­ tems are pairs "set of contexts, set of bridge rules". We write {A, i) to mean A and that A ELi. We say that A is an Li-wff to mean that A E Li. The formal definition of deduction of an MC system is given in [Giunchiglia, 1993] .)

Definition 3.1 (MBI) Let P be a set of primitive propositional/etters. An MC system MBI = { { c, I}, .6.cr) is such that:

• (i) c = (Lc, Tc}· Lc is a propositional language whose atomic formulas are P and IB( "A") for any for­ mula A in Lr. Lc is closed under the proposi­ tional connectives. Tc = C(flc, .6.c)· .6.c is correct and complete for propositional logic.
• (ii) I = (Lr, Tr). Lr is a propositional language whose atomic formulas are P. Lr is closed under the propositional connectives. Tr = C(flr, .6.r ). .6.r is correct and complete for propositional logic.
• (iii) .6.cr is the following set of bridge rules:

Restrictions: Rup.I can be applied only if the in­ dex of every undischarged assumption {A, I) de­ pends on, is equal to c.

MBI was already discussed in [Giunchiglia and Ser­ afini, 1991]. Rup.l and Rdn.I are called reflection up and reflection down respectively. Rdn.I allows to derive A in I from the fact that IB( "A") has been derived in c. Rup.I has a similar reading. The restriction on Rup.I is needed to preserve the correctness of c.

3.2 Implicit and Explicit belief

One approach to the formalization of non logical omniscience is based on the distinction between ex­ plicit beliefs and implicit beliefs. According to Levesque [Levesque, 1984], while explicit beliefs are the set of effective beliefs of the agent, implicit beliefs model what the world would be like if what he believed were true. Implicit belief is used as a limit notion which gives an upper bound to what a real agent can ever believe. No matter what it explicitly believes, it will never explicitly believe more than its implicit beliefs. In this context, a natural step is to take the agent's implicit and explicit beliefs as the beliefs of an ideal reasoner I and of its real­ ized version E, respectively. The intuition is in fact the same, that is that I I implicit belief is the limit idealized version of E I explicit belief. However the emphasis is slightly changed as we do not care of how the world is but only of the subjective view of I. Implicitly we as­ sume that the world is how I assumes it is, but this is irrelevant from a technical point of view.

Thus, if we want to model a situation where c can rea­ son about the idealized and real capabilities of an agent, we have to have two contexts I and E and two belief predicates, that is IB aod EB. As we want c to be a per­ fect believer for I and E, we have the two reflection rules for each of the two contexts. Figure 2 gives a structural description of the resulting MC system, called MBIE. The formal definition follows:

Definition 3.2 (MBIE) Let P be a set of pnm·­ tive propositional letters. An MC system MBIE = ( { c, I IE}' .£l.,r u a.,E) is such that:

• (i) c is as in definition 9.1 with the atomic formulas of L., extended to contain also EB("A"), for any formula A E Lr;
• (ii) I is as in definition 9.1;
• (iii) ll..,r is as in definition 9.1;
• (iv) E = (LE,TE) with PE ~ Pr, WE~ Wr, nE ~ Or and ll.E ~ ll.r;
• (v) ll.Ec is the following set of bridge rules:

Restrictions: 'Rup.E can be applied only if the in­ dex of every undischarged assumption (A, E) de­ pends on, is not equal to E; ndn.E can be applied only if A is a LE-wff.

Some observations. E is defined to be the realized version of I. According to clause ( i), even if a certain formula A is not an LE-wff, EB("A") is a wff of Lc . This allows us to say in c that A is not explicitly believed (-.EB("A")).

3.3 Local reasoning

Underlying all the above definitions is the intuition that a reasoner can use all its construction rules on all its basic facts . However, it is well known that human beings have difficulty in putting together all the information they possess. Human memory seems structured in frames of mind hardly communicating between them [Stalnaker, 1984] . Reasoning happens locally to each frame and hardly interacts with the reasoning performed in other frames. Thus, for instance, we never think of Africa and a fl at tire at the same time . The obvious way to model this situation is to associate to each agent a set of rea­ soners E1 , . . . ,En, one for each frame of mind , variously interconnected among themselves and with c. This can be done in many different ways, each modeling a different intuition. In the following we discuss one very general possibility.

As usual cis connected to I via reflection up and reflec­ tion down. We suppose that the various E; have different languages and different sets of inference rules. We have a reflection up rule between c and each E;. This guar­ antees the completeness of c. However we have only one predicate EB for all frames and no reflection down rules into the frames. This models the intuition that c has a correct view of what is explicitly believed but without knowing in which frame theorems are proved . EB("A") means that there is at least one frame of mind in which A is true. A weak form of reflection down and there­ fore a weak notion of correctness for c can still be given. Suppose that we have n frames E1 , ... , En of which A is a formula. Suppose that in all such frames but E1 , as­ suming A we derive a formula B that we do not believe. Then, as a consequence, A must be believed in E1 . This models the intuition that, still not knowing a priori in which frame a theorem is proved, c can sometimes infer this by evaluating all the possibilites. The structure of the resulting system, called MBIE(n), is given in figure 3. Its definition is as follows .

Definition 3.3 (MBIE(n)) Let P be a set of primitive propositional letters and n a natural number. An MC system MBIE(n) = ( { c, I, { E; }t::;;::;n }, D.c1 U D.cE(n)) iS such that:

• (i) c is as in definition 3.2;
• (ii) I is as in definition 3.2;
• (iii) D.cl is as in definition 3.2;
• (iv) Each E; = (LE; , TE;) is defin ed the same as E in definition 3.2;
• (v) DocE(n) contains bridge rules nup.E;, {1 ~ i ~ n}:

and bridge rules ndn.E·, , (1 ~ k1 ... km ~ n) :

Restrictions: nup.E; can be applied only if the in­ dex of every undischarged assumption (A, E;) de­ pends on, is not equal toE; ; in the rule ndn.E., ' k1 , k2 , ... , km are all the indexes such that A is a wff of the corresponding frame .

Definition 3.3 generalizes definition 3.2 of MBIE in the sense that E has been substituted with n frames .

Notice that, starting from the intuition that a reasoner can be modeled as a logical theory, we have introduced various forms of non logical omniscience and associated them to a particular structural part of E. The resulting system MBIE(n) models all of them. This process is exhaustive in the sense that all the structural subparts of E have been considered (that is its language, its theorems and E itself). If one accepts the abstract characterization of reasoners as contexts, this process is exhaustive also in the sense that it considers all the possible forms of non logical omniscience. Experimentally, so far we have failed to find a form of non logical omniscience which cannot be modeled as composition of the basic forms defined above. In particular, all the forms of lack of logical omniscience defined in the past that we are aware of can be uniformly reconstructed (see next section Cor some hints of how this can be done).

It can be proved that the following proposition holds (f-Ms is the consequence relation defined by the MC sys­ tem MS):

Proposition 3.1 For any Lr-wff At. A2 and any LE,­ wff 81, 82:

• (i) if A1 is a classical tautology then lt.ta1E(n) (IB("A1"), c};
• (ii) f-MBIE(n) {JB("A1") /1. IB("A1 :J A2") :J IB("A2"), c);
• (iii) if (AI, I) f-MBIE(n) (A2, I), then f-MBIE(n) (IB("A1") :::> IB("A2"), c};
• (iv) if (81, E;) f-MaiE(n) (82, E;} for any 1 $ i $ n, such that 81 and 82 are LE, -wff, then rMBIE(n) (EB("81") :::> EB("B2"), c) .
• (v) if Oc = 0, then if f-MBIE(n) (EB("8t"), c} then f-MBIE(n) (IB("8t"), c).

Item (i) says that all classical tautologies are implicitly believed. Item (ii) says that implicit belief is closed un­ der implication. Item (iii) says that implicit belief sim­ ulates (in c) deduction in I . Item (iv) states the same property as (iii) for explicit belief. Item (v) says that explicit beliefs are implicitly believed. This is in fact a consequence of the fact that TE, (_;T1, with 1 $ i $ n. However, from the point of view of c, there is no apparent relation between E's theorems and /'s. c can be made aware of this relation by adding a new set of bridge rules each connecting a frame E; to I saying that a formula can be derived in I because of it has been derived in E;.

Definition 3.4 (MBIE'(n)) MBIE'(n) is an MC sys­ tem obtained from MBIE(n) by adding, for all frames E; the following bridge rule:

Adding E;2I models the intuition that c knows that E believes a subset of I's beliefs and that explicitly uses this information to build proofs in /. Adding E;2/ does not change what is believed by I and E. However in MBIE'(n), EB("A") :::> IB("A") is a theorem of c (while this is not the case for MBIE(n)).

Proposition 3.2 For each LE,-Wff A, rMBIE'(n) (EB("A") :::> IB("A"), c) .

4 Some important instances

It is now interesting to specialize definition 3.3 of MBIE(n) to consider MC systems where each form of lack of logical omniscience is taken in isolation. This al­ lows us to define interesting MC systems some of which can be proved equivalent to the various systems defined in the past (for instance all those in [Fagin and Halpern, 1988; Levesque, 1984; Konolit;e, 1984]). In t.he follow­ ing we study, the situation of lack of aWMeness. Let us consider the following MC system.

Definition 4.1 (MLL, MLL') Let MLL (MLL') be an MC system obtained from MIEB(J) (MIEB'(J)) by impo.sing PE -< Pr and tl.E = tl.r.

The intuition behind MLL and MLL' is very similar to that behind Fat;in and Halpern's lopic of general aware­ ness (called LAW from now on) lFagin and Halpern, 1988]. In LAW an agent explicitly believes a subset of the formulas he is aware of. This is obtained by extending the modal language with a modal operator of awareness, AW. An agent explicitly believes a if and only if he is aware of a and implicitly believes it, in formulas

(1) is in fact an axiom schema of LAW. Suitable axioms define the set of formulas of which the agents are aware of, e.g. there may be axioms stating that awareness is closed with respect to certain subformulas. MLL, MLL' and LAW can be proved to prove exactly the same set of implicit and explicit beliefs (by taking the obvious translation where modal . operators are translated into unary predicates. For any modal formula A, we write A+ to mean its first order translation) 2 ·

Theorem 4.1 Let LAW a system for general awareness such that all the axioms involving A W but {1} are of the form AWo1 /1. ·· · I\ AWon :::> AWo with n 2: 0. Then, for any Lc-wff A, rwLL (A, c} (1-MLL' (A, c)) if and only iff-tAw A+.

(The condition on the axioms involving AW does not involve anything deep and could be lifted away. We have imposed it to guarantee not circular definitions of MC systems. In principle one could use A W to define L E in terms of TE .) However the inverse of theorem 4.1 cannot be proved, i.e. LAW cannot be proved equiva­ lent to MLL nor to MLL'. Notice that in theorem 4.1 we quantify over Lc-wffs and not over the wffs in LAW. The problem is that LAW's language contains the modal op­ erator A W which does not have any counterpart in MLL or MLL'. This can be easily solved by adding a monadic awareness predicate A W to Lc and by making sure that the formulas of the kind AW("a") belong to Tc, subject to the restriction that a is a formula of LE. This step makes the translation of one direction of axiom (1), that is EB("A") :::> IB("A") /1. AW("A") a theorem of MLL' (but not of MLL). However this is not the case for the other direction, that is IB("A")!I.AW("A") :::> EB("A"). This effect can be obtained by adding MLL' the axiom AW("A") = IB("A") :::> EB("A") and a new bridge rule, called I2E, which allows to derive A in E whenever A has been derived in I, subject to the restriction that A is a wff in LE.

2 All the modal systems considered in this paper are given semantically. In comparing a semantically presented modal system S1 with an MC system M S1, we say that S1 and M S1 are equivalent, i.e. A1, ... , An Fs A if and only if I (At, c), ... ,(A~, c) f-Ms 1 (A+, c).

Definition 4.2 (MLA W) Let MLA W be an MC sys­ tem obtained from MLL' by extending Lc with the monadic predicate AW, Oc with the axiom AW("A") = IB("A") :::> EB("A") and by adding the following · bridge rule:

Restriction: A is an LE-wff.

Theorem 4.2 LAW and MLA Ware equivalent.

In order to get the equivalence result with LAW we had to extend MLL in various ways. However it should be clear that MLL (and not MLAW) satisfies all and only the minimal structural properties of agents with lack of awareness, that is the fact that LE C LJ. The extra conditions satisfied by MLA W do not change the beliefs of I and E (theorem 4.1). Their effect is to allow c to prove more and more facts about the lack of logical omniscience of E (proposition 3.2, theorem 4.2). How­ ever, while the addition of A W to Lc and of E12/ to the set of bridge rules of MLL has an intuitively plausi­ ble interpretation, this is not the case for I2E. /2E says that an implicit belief which can be expressed in the lan­ guage of LE is also an explicit belief. As a consequence, it allows derivations (in general not possible otherwise) where explicit beliefs are first proved in I and then ex­ ported to E. However we do not find derivations of this kind intuitively plausible as we think that E's deductive capabilities should not exploit /'s. Finally, the axiom added to MLL' to obtain MLAW seems to exist mainly for technical reasons.

As a general observation, the advantages over a single theory approach should now be clear. In MC systems, localization (of the language, of the axioms, of the de­ ductive machinery) is intrinsic in the logic, namely in the fact that we have distinct contexts. The properties of an agent can be directly imposed on the contexts rep­ resenting it and not, as it is the case in a single theory approach, in some global theory of the world (playing the role of c) . This allows for easier (to do and to under­ stand) formalizations where each agent is locally defined independently of anything else.

5 Example

Let us consider MBIE(2), that is the MC system that for­ malizes the beliefs of an agent with two frames of mind. The following wff is provable in MBIE(2) .

Intuitively it says that if A, B and G are explicit beliefs, then there is a frame where one among A A B, A A G and BAG is provable. Notice that, as a consequence, at least two among A, B and G are formulas of this frame. The proof is given in figure 5. Notice that inside each context we use Natural Deduction and some deciders, e.g. the de­ cider for propositional logic TAUT [Giunchiglia, 1992]. The proof in figure 5 can be summarized as follows. We proceed by contradiction and assume in context c the hypothesis, i.e. EB("A")AEB("B")AEB("G") (line 4) and the negation of the conclusion, i.e . ...,EB("A A B"),

-,EB("A A G") and ...,EB("B A G") (line 5) . Assum­ ing B in E1 (line 2), from the fact that EB("A" ) and -,EB("A A B") are derived inc (lines 6, 7) and from the fact that there are only two frames, we conclude that A is derivable in E2 . (line 8). The hypothesis EB("G") (line 11) and the fact that there are two frames implies that G must be derivable in E1 or in E2. In the first case we have BAG in E1 (line 14) which implies EB("BAG") in c but this leads us to a contradiction (line 16) . Ex­ actly the same argument can be given for E2 and A A G (lines 10, 12). This allows us to infer A in (line 17) and then A A B in E2 (line 29). Reflecting up A A B (line 30) allows us to derive the goal by propositional reasoning in c (line 34).

A first observation is that the agents' contexts are used to prove theorems which are then reflected up (e .g. line 30). This is a practical consequence of the fact that agents are not simulated in c but are rather "used" to extract what it is proved in their contexts. In this per­ spective reflection down is used as a means to impose a set of facts into a context (e.g. lines 8, 13, 17). Notice that all the applications of reflection down are above all the applications of reflection up. This is in fact the gen­ eral way of performing reasoning with MC systems for belief: (i) first some conjectures are made in c; (ii) then these conjectures are "imposed" on the reasoners (via reflection down); (iii) then the reasoning capabilities of the reasoners are used to compute the consequences of the conjectures; (iv) finally the result is exported back to c via reflection up. Some amount of propositional rea­ soning can be performed in c before step (i) and after step (iv).

6 Conclusion

In this paper we have proposed a new approach to the formalization of reasoning about belief where agents are modeled as sets of interacting contexts. In this frame­ work the properties of each agent can be directly formal­ ized by imposing local suitable conditions on the theories modeling it (that is, on the language, on the axioms, on the deductive machinery, on the bridge rules) .