All They Know: A Study in Multi-Agent Autoepistemic Reasoning

1 Introduction

While the study of nonmonotonic reasoning formalisms has been at the forefront of foundational research in knowledge representation for quite some time, work in this area has concentrated on the singl~agent case with only few exceptions.

This focus on single agents is somewhat surpris­ ing, since there is little doubt that agents, who have been invested with nonmonotonic reasoning mechanisms, should be able to reason about other agents and their ability to reason nonmonotonically as well. For exam­ ple, if we assume the common default that birds nor­ mally fly and if Jill tells Jack that she has just bought a bird, then Jill should be able to infer that Jack thinks that her bird flies . Multi-agent nonmonotonic reasoning is also crucial when agents need to coordinate their ac­ tivity. For example, assume I promised a friend (who is always on time) to meet him at a restaurant at 7PM. Ifl leave my house knowing that I will not make· it there by 7PM, I will probably not change my plans and still go to the restaurant . After all, I know that my friend has no reason to believe that I am not on my way to meet him and that he will therefore wait for me. Note that I reason about my friends default assumption to wait in this case. Other examples from areas like planning and temporal projection can be found in [Mor90].

One of the main formalisms of nonmonotonic reason­ ing is autoepistemic logic (e.g. [Moo85]). The basic idea is that the beliefs of agents are closed under perfect in­ trospection, that is, they know 1 what they know and do not know. Nonmonotonic reasoning comes about in this framework in that agents can draw inferences on the basis of their own ignorance. The following exam­ ple by Moore illustrates this feature: I can reasonably conclude that I have no older brother simply because I do not know of any older brother of mine. A partic­ ular formalization of autoepistemic reasoning is. due to Levesque [Lev90], who proposes a logic of only-knowing ( OL), which is a classical modal logic extended by a new modality to express that a formula is all an agent be­ lieves. An advantage of this approach is that, rather than having to appeal to non-standard inference rules as in Moore's original formulation, OL captures autoepis­ temic reasoning using only the classical notions of logical

consequence and theoremhood.

In this paper, we propose a propositional multi-agent extension of OL. We provide a formal semantics within the possibl~world framework and a proof theory, which is complete for a large fragment of the logic. The new logic also leads us to natural extensions of notions like stable sets and stable expansions, which were originally developed for the single-agent case.

General multi-agent nonmonotonic reasoning for­ malisms have received very little attention until recently. 2 A notable exception is work by Morgen­ stern and Guerreiro [Mor90, MG92], who consider both multi-agent autoepistemic reasoning and multi-agent cir­ cumscription theories. On the autoepistemic side, they propose multi-agent versions of stable sets, which allow agents to reason about other agents' nonmonotonic inferences. In contrast to our work, however, these stable sets are not justified by an independent seman­ tic account. Recently, and independently of our work, Halpern [Hal93] also extended Levesque's logic OL to the multi-agent case. While Halpern's logic and ours share many (but not all) properties, the respective model theories are quite different. In particular, while our ap­ proach remains within classical possible-world semantics, Halpern uses concepts very much related to the so-called knowledge structures of [FHV91] . Using the same tech­ nique, Halpern also extends the notion of only-knowing proposed in [HM84] to the multi-agent case. There, how­ ever , agents are not capable of reasoning about other agent's nonmonotonic inferences because only-knowing is used only as a meta-logical concept.

1 While we are concerned with belief and, in particular, allow agents to have false beliefs, we nevertheless use the

terms knowledge and belief interchangeably.

2 There has also been work applying nonmonotonic the­ ories to special multi-agent settings such as speech acts (e.g. (Per87, AK88]). Unlike our work, these approaches are not concerned with general purpose multi-agent nonmono­

tonic reasoning.

The rest of the paper is organized as follows. Section 2 defines the logic OLn, extending Levesque's logic of only­ knowing to many agents. Besides a formal semantics we also provide a proof theory, which is complete for a large fragment of OLn. Furthermore, we look at the proper­ ties of formulas in OLn, which uniquely determine the beliefs of an agent and are thus of particular interest to knowledge representation . Section 3 considers examples of multi-agent autoepistemic reasoning as modeled by OLn . Section 4 shows how OLn yields natural multi­ agent versions of stable sets and stable expansions. Fi­ nally, we summarize the results of the paper and point to some future work in Section 5.

2 The Logic OLn

After introducing the syntax of the logic, we define the semantics in two stages. First we describe that part of the semantics that does not deal with only-knowing. In fact, this is just an ordinary possible-world semantics for n agents with perfect introspection . Then we introduce the necessary extensions that give us the semantics of only-knowing. Finally, we present a proof theoretic ac­ count , which is complete for a large fragment of the logic, and discuss properties of the logic which are important in the context of knowledge representation.

2.1 Syntax

Definition 1 The Language O.Cn

The primitives of O.Cn consist of a countably infinite set of atomic propositions (or atoms), the connectives V, -. , and the modal operators L; and 0; for 1 ~ i ~ n . (Agents are referred to as 1, 2, ... , n.) Formulas are formed in the usual way from these primitives. 3 L;a should be read as "the agent i believes a" and O;a as "a is all agent i believes. " A formula a is called basic iff there are no occurrences of 0; (1 ~ i ~ n) in a .

Definition 2 A modal operator occurs at depth n of a formula a iff it occurs within the scope of exactly n modal operators.

3 We will freely use other connectives like /\, :::> and :::, which should be understood as syntactic abbreviations of the usual kind.

For example, given a= pt\L1L2(L3qV-.02r), L1 occurs at depth 0, L2 at depth 1, and L3 and 02 occur both at depth 2.

Definition 3 A formula a is called i-objective (fori = 1, ... n) iff every modal operator at depth 0 is of the form Oj orLj withi::f=j .

In other words, i-objective formulas talk about the ex­ ternal world from agent i's point of view, which includes beliefs of other agents but not his own. For example, (pVL2q)A-.03L1p is !-objective, but (pVL2q)A-.L1 03p is not .

Definition 4 A formula a is called i-subjective iff ev­ ery modality at depth 0 is of the form L; orO, and every atom occurs within the scope of a modal operator.

That is, i-subjective formulas talk only about what agent i believes. For example, L1pt\-.01p is !-subjective, L1pt\ q and L1p t\ L2q are not .

2.2 The Semantics of Basic Formulas

Basic formulas are given a standard possible-world se­ mantics [Kri63, Hin62, Hin71], which the reader is as­ sumed to be familiar with. 4 Roughly, a possible-world model consists of worlds, which determine the truth of atomic propositions, and binary accessibility relations between worlds. An agent's beliefs at a given world ware determined by what is true in all those worlds that are accessible to the agent from w. Since we are concerned with agents who possess perfect introspection, we restrict the accessibility relations in the usual way, that is, they are both transitive and Euclidean. 5 The resulting logic is called K45n or weak S5n . 6

Definition 5 A K45n-Model

M = {W, 1r, R1 , . .. , R,.) is called a K45n-model (or simply model) iff

1. W is a set (of worlds).
2. 1r is a mapping from the set of atoms into 2w.
3. Ra ~ W x W for 1 ~ i ~ n .
4. Ra is transitive and Euclidean for 1 ~ i ~ n.

Given a model M = {W, 1r, R1, .. . , R,.) and a world w E W, the possible-world semantics of basic formu­ las is defined as follows: Let p be an atom and a and f3 arbitrary basic formulas.

wf=p ¢::::::} wE 1r(p)

wf=-.a ¢::::::} wl;ea

wf=a V f3 ¢::::::} wf=a or wf=/3

wf=L1a ¢::::::} for all w', if wRaw' then w'f=a

A set of basic formulas r is satisfiable iff there is a model M = (W, 1r, R1, . .. , R,.) and wE W such that wf=1 for all1Ef.

In the single-agent case, Levesque made use of the fact that the semantics of K451 has a much simpler formula­ tion. There we can assume a fixed set of worlds, which is the set of all truth assignments. A model then consists of a world w, which corresponds intuitively to the real world, and a set of worlds W, which determine the beliefs of the agent. There is no need for an explicit accessibil­ ity relation, since the worlds in M are globally accessible from every world and a sentence is believed just in case it is true at all worlds in W. Unfortunately, such a sim­ ple model does not extend to the multi-agent case and we are forced to a more complicated semantics with ex­ plicit accessibility relations as defined above. 7 For this reason, the extension of Levesque's logic OL to many agents turns out to be a non-trivial exercise.

'See (HC84, HM92] for an introduction.

~ R; is Euclidean iff Vw, w', w", if wR;w' and wR;w", then w'R;w".

6 The subscript n indicates that we are concerned with the n-agent case.

2.3 The Canonical Model

It is well known that, as far as basic formulas are con­ cerned, it suffices to look at just one, the so-called canon­ ical model [HC84, HM92]. This canonical model will be used later on to define the semantics of only-knowing.

The central idea behind canonical models are maxi­ mally consistent sets.

Definition 6 Maximally consistent sets

Given any proof theory of K45n and the usual notion of theoremhood and consistency, a set of basic formulas r is called maximally consistent iff r is consistent and for every basic a, either a or -,a is contained in r.

The canonical K45n-model Me has as worlds precisely all the maximally consistent sets and a world w' is Rs­ accessible from w just in case all of i's beliefs at w are included in w'.

Definition 1 The Canonical K45n-Model Me The canonical model Me = {We, 11', Rt, ... , Rn} zs a Kripke structure such that

1. We = { w I w is a maximally consistent set}.
2. For all atoms p and wE We, wE 1r(p) iff pEw.
3. wRaw' iff for all formulas L;a, if L;a E w then a E w'.

The following (well known) theorem tells us that noth­ ing is lost from a logical point of view if we confine our attention to the canonical model.

Theorem 1 Me is a K45n-model and for every set of basic formulas r, r is satisfiable iff it is satisfiable m Me.

2.4 The Semantics of All They Know

Given this classical possible-world framework, what does it mean for an agent ito only-know, say, an atom pat some world w in a model M? Certainly, i should believe p, that is, all worlds that are i-accessible from w should make p true. Furthermore, i should believe as little else as possible apart from p. For example, i should neither believe q nor believe that j believes p etc. Minimizing knowledge using possible worlds simply means maximiz­ ing the number of accessible worlds. Thus, in our ex­ ample, there should be an accessible world where q is false and another one where j does not believe p and so on. It should be clear that in order for w to satisfy only-knowing a this way, the model M must have a huge supply of worlds that are accessible from w. While not essential for the definition of only-knowing, it turns out to be very convenient to simply restrict our attention to models that are guaranteed to contain a sufficient sup­ ply of worlds. 8 In fact, we will consider just one, namely the canonical model of K45n. Let us call the set of all formulas that are true at some world w in some model of K45n a world state. The canonical model has the nice property that it contains precisely one world for every possible world state, since world states are just maxi­ mally consistent sets.

7 1n essence, if we ha.ve more tha.n 1 agent a.nd a. global set of worlds for ea.ch agent, the agents would be mutually introspective, which is not wha.t we wa.nt.

With that agent i is said to only-know a formula a at some world w (in the canonical model) just in case a is believed and any world w' which satisfies a and from which the same worlds are i-accessible as from w is itself i-accessible from w. We now turn to the formal definitions.

Definition 8 Given a model M = (W, 1r, Rto ... , Rn} and worlds w and w' in W, we say that w and w' are i­ equivalent (w ~i w') iff for all worlds w· E W, wRaw* iff w'Raw*.

Given an arbitrary formula a of OCn, a world w in a model M, let

wf=O;a {:::::} for all ti/ s.t. w ~; w', wRaw' iff w'f=a.

A formula a of 0 Cn is a logical consequence of a set of formulas r iff for all worlds w in the canonical model Me, if wf=-y for all-y E r, then wf=a. As usual, we say that a is valid ( f=a) iff {} f=a. A formula a is satisfiable iff ..,a is not valid.

Note that Theorem 1 guarantees that OLn restricted to basic formulas is still simply K45n.

A superficial comparison of the rules for 0; and L; suggests that they differ at two places. For one the 0;­ rule quantifies over i-equivalent worlds only. For another, the "if ... then" of the L;-rule is replaced by an "iff." While the latter is significant, it can be easily shown that we can restrict the L;-rule to quantify over i-equivalent worlds as well.

Lemma 2.1

For any K45n-model M and world w in M,

wf=L;a {:::::} for all w' s.t. w ~; w', if wRaw' then w'l=a

2.5 A Proof Theory

In order to obtain a proof theory for a large fragment of OLn, we apply the same idea Levesque used to axiom­ atize his logic OL. The idea is to add a dual operator N; for every L; to the language OCn, which we refer to as O.NCn. While L;a can be read as "agent i knows at least a," N;a should be read as "agent i knows at most that a is false." O;a now becomes simply an abbrevi­ ation for L;a A Nr-·a, that is, agent i believes only a iff he believes at · least and at most a. We extend the notion of an i-subjective or i-objective formula to cover the N;-operators as well. For example, ..,LtP AN 1...,L2p is both !-subjective and 2-objective.

8 1n Levesque's OL, this is automatically given since worlds a.re drawn from the fixed set of all truth assignments.

The semantics of N, is as follows. N,a is true at a world w iff a is true at all i-equivalent worlds of w which are not accessible from w. In the formalization it is convenient to add new accessibility relations Rs for just these non-accessible worlds to the canonical K45n­ model. This way, the N, behave just like ordinary K45 belief operators.

Definition 9 The Extended Canonical Model

Given the canonical model Me= (We, 1r, R1 , ... , Rn), let the extended canonical model be

where for all w, w' EWe, wRsw' iff w ~~ w' and w.ftaw'.

Lemma 2.2 The Rs are transitive and Euclidean.

Given the extended canonical model Mee and a world wE We, the semantic rule for N, is simply:

Notions like logical consequence and validity for this ex­ tended logic are defined as for OLn with Me replaced by Mee ·

Given Lemma 2.2, it is obvious that the N1 have all the properties of a K45n·Operator. Moreover, if we view L, and N, as two different agents, then the L,-agent knows exactly which worlds the N,-agent can see and vice versa. In other words, the L;-agent and N;-agent are mutually introspective. For example -,L;p :::> N;...,L;p is valid. Finally, note that for every equivalence class of worlds W, under ~~, Rs and Rs cover all worlds in W, ex­ haustively, that is, taken together, the two relations form a complete sub graph over W,. This feature is reflected in valid formulas of the form N;a :::> ...,L;a for falsifiable a .

Axioms:

• A1 Axioms of propositional logic

A2 L,(a :::> /3) :::> (L,a :::> L;/3)

A3 N;(a :::> /3) :::> (N,a :::> N;/3)

A4 u :::> L,u I\ N;u for all i-subjective u

A5 N;a :::> ...,L;a for all basic i-obj . a falsif. in K45n

A6 O;a = (L,a I\ N;...,a) for all a

Inference Rules:

MP From a and a:::> f3 infer /3.

Nee From a infer L,a and N,a.

Note that A2-A4 imply that the L, and N, have all the properties of regular K45n·Operators. Also, A4 not only gives us the regular introspection axioms of K45n but also cross axoms (mutual introspection) such as ...,L,a :::> N,...,Lia. A5 provides the crucial link between L, and N; capturing the relationship between "knowing at least" and "knowing at most ." 9

Theorem 2 Soundness

Given the usual definition of theoremhood (I-) with re­ spect to the above proof theory, for all a in ON Cn, ' ifl-a then f=a.

9 Levesque, in his· axiomatization of OL, uses a special case of this axiom. In his case, a ranges merely over the falsifiable formulas of classical propositional logic (no modalities) .

Notice that axiom A5 assumes that a ranges only over basic i-objective formulas. We need this restriction in or­ der to appeal to falsifiability in the existing logic K45n . 10 For the axiomatization to be complete, such a restric­ tion essentially requires that arbitrary formulas N,/3 or Ls/3 are reducible to equivalent forms N,p· and L,p·, where /3* is a basic formula, that is a formula without any N; 's. That, however, is not true in general. For example, LaN;p and NaL;NsP are not reducible for dis­ tinct i and j. However, if we rule out such cases, the proof theory is indeed complete for the restricted lan­ guage, which we call ON c;;.

Definition 10 The Language ON£;;

a is a formula of ON£;; iff a is a formula of ON Cn and, after replacing every occurrence of 0,/3 within a by its definition Ls/3 I\ N,...,p, no N; may occur within the scope of anN, or L, fori f. j.

For example, while N,L,...,N,p and N,(L;p V N1-,p) are in ON£;;, N,N;p and N,L;N,p are not for distinct i and j.

Theorem 3 Completeness For ON£;;

For all aEON£;;, if f=a then 1-a.

Proof: The proof is an adaptation of Levesque's com­ pleteness proof for OL [Lev90]. ·

(Halpern recently proved that the above proof theory is indeed not complete for all of OLn.)

Given Theorem 2 and 3, it is not hard to prove that 0£1 is equivalent to the propositional version of Levesque's logic OL because Levesque's proof theory is a special case of ours.

Theorem 4 0£1 and OL are equivalent

A formula a in 0£1 is a theorem of OL1 iff a is a theorem of OL.

We introduced the operator N, mainly for the purpose of obtaining a proof theory for OLn. Except for a for­ mal derivation using the axioms in Section 3, we will no longer be concerned with the N,-operators in the rest of the paper and go back to the original OLn and its language OCn.

2.6 i-Determinate Sentences

We now turn to a class of formulas which are of par­ ticular interest to knowledge representation, since they determine, when only-known, precisely what an agent believes and does not believe.

Definition 11 i-Determinate Formulas 11

A formula a E OCn is i-determinate iff

1. there is a world w in Me such that wf=O,a and
2. for all worlds w', ifw'f=O,a then w ~~ w'.

The following theorem demonstrates that i-determinate formulas indeed deserve their name.

Theorem 5 For all a E OCn, a is i-determinate iff for all /3, exactly one of O;a :::> L,/3 and O,a :::> ...,L,/3 is valid.

10 Note that this peculiar axiom schema is recursive since falsifiability in propositional K45n is decidable.

11 In the single-agent case, the analogous concept of determinate formulas was defined in [Lev90]. ·

What are examples of determinate formulas? In the single-agent case, it has been shown that all objective formulas (no modalities at all) are determinate. Not surprisingly, objective formulas are also i-determinate. In fact, this result can be generalized to include all basic i-objective formulas.

Theorem 6

All basic i-objective formulas are i-determinate.

Other examples of i-determinate formulas, which are not i-objective, include -.L;-.p:) p and -.L;Ljp:) -.Ljp, which allow agents to reason nonmonotonically and are discussed in more detail in Section 3.

So far we have only considered basic i-determinate sentences. Does the above result extend to non-basic i-objective formulas as well? The answer, surprisingly, is: sometimes but not always! For example, it is not hard to show that the formula Ojp (where pis an atom) is also i-determinate, that is, the beliefs of agent i are uniquely determined if all i knows is that all j knows is p. However, the formula -.Ojp is not i-determinate because t=-.O;-.Ojp. 12 In other words, it is impossible for i to only-know that j does not only-know p. Intuitively, for i to know that j does not only-know p, i needs to have some evidence in terms of a basic belief or non-belief of j. It is because of properties like t=-.0;-.0jp that our axiomatization is not complete for all of ON .Cn.

3 Multi-agent Nonmonotonic Reasoning

While our axiomatization is complete only for a subset of OLn, it is nevertheless strong enough to model interest­ ing cases of multi-agent nonmonotonic reasoning. Here are two examples:

1. Let p be agent i's secret and suppose i makes the following assumption: unless I know that j knows my secret assume that j does not know it. We can prove in OLn that if this assumption is all i believes then he indeed believes that j does not know his secret. Formally 1- 0;(-.L;Ljp:) -.Lip):) L;-.Ljp. 13

A formal derivation of this theorem of OLn can be ob­ tained as follows. Let a= -.L;Ljp:) -.LiP· The justifi­ cations in the following derivation indicate which axioms or previous derivations have been used to derive the cur­ rent line. PL or K15n indicate that reasoning in either standard propositional logic or K45n is used is without further analysis.

To see that i's beliefs may evolve nonmonotonically given that i only-knows a, assume that i finds out that j has found out about the secret. Then i's belief that j does not believe the secret will be retracted. Formally 1- O;(Ljp 1\ ( -.L;Ljp:) -.Lip)) :) (-.L;-.Ljp 1\ L;Ljp). Notice that, while OLn is itself a regular monotonic logic, the nonmonotonicity of agent i's beliefs is hidden within the 0;-operator.

12 ln contrast, O;...,Ojp is satisfiable in Halpern's logic.

13 Note that if we replace Ljp by p we obtain regular single­ agent autoepistemic reasoning.

Finally, -.L;Ljp:) -.Ljp is also i-determinate. In particular, 0;(-.L;Ljp:) -.Ljp) = 0;-.Ljp is valid.

1. Now let p stand for the old "Tweety flies." As expected, we obtain 1- Oj(-.Lj-.p:) p) :) LjP· (Not sur­ prisingly, -.Lj-.p:) p is j-determinate.) By the rule of necessitation and the distribution axiom for belief we immediately get 1- L;Oj(-.Lr'P:) p) :) L;LjP· In other words, i is able to reason about j's ability to reason non­ monotonically, essentially by simulating j's reasoning.

It should be pointed out that an assumption like i knows that all j knows is a is certainly unrealistic in general and is related to what Morgenstern calls arro­ gance (Mor90]. It would be much more reasonable if we could say that i knows that a is all j knows about some relevant subject, say Tweety. In fact, we have proposed such a notion of only-knowing-about as an extension of OLn in (Lak93] . There we also show that only-knowing is often a good approximation of only-knowing-about in the sense that, if we restrict ourselves to beliefs that are only about the subject matter in question, 14 then the be­ liefs that follow from only-knowing-about are the same as those that follow from only-knowing.

4 i-Stable Sets and i-Stable Expansions

Single-agent autoepistemic logic was originally devel­ oped using the concepts of stable sets (StaBO] and sta­ ble expansions (Moo85] . Here we define natural n-agent extensions of these notions and show how they relate to OLn. For the purposes of this paper, we confine our­ selves to basic formulas only.

Definition 12 i-Epistemic State

A set of basic formulas r is called an i-epistemic state iff there is a world w in Me such that for all basic j, wt=L;j iff i E f.

Definition 13 i-Stable Sets

Let r be a set of basic formulas . r is called i-stable iff

1. r contains all valid formulas of K45n.
2. If a E r and a :) /3 E f then /3 E f.
3. If a E r then L;a E f.
4. If a¢ r then -.L;a E r.

Note that the only difference between i-stable sets and the original definition of stable sets lies in condition 1. While stable sets are only required to contain the tau­ tologies of regular propositional logic, i-stable sets must contain all K45n·Valid formulas.

The next theorem proves that i-stable sets and i­ epistemic states are equivalent notions. In other words, the definition of i-stability falls out naturally given the semantics of OLn.

14 The subject matter is defined as a set of atomic proposi­ tions 11'. The restriction says that the atoms occurring within a belief must be contained in 11'.

Theorem 1

Let f be a set of basic foNnulas . r is i-stable iff r is an i-epister.nic state.

Halpern arrived at the same notion of i-stability inde­ pendently [Hal93]. He also considered definitions based on logics other than K45n .

Given a set of basic formulas r, let r {r I! is basic and I fl. r}, L;f = {Ln I for all/ E r}, and -,L;f = {-,Ln I for all/ E r}.

Definition 14 i-Stable Expansion

Let A be a set of basic forr.nulas and let f=K45 denote logical consequence in K45n. r is called an i-stable ex­ pansion of A iff r = {basic II Au L;f u -,L;fpK45l}.

The definition of i-stable expansions looks exactly like Moore's definition of stable expansions except that we use logical consequence in K45n instead of logical conse­ quence in propositional logic. Using the stronger K45n is necessary in the multi-agent case, since an agent knows that other agents are also perfectly introspective. For example, if agent i believes -,LiP for a different agent j then he also believes Lj-,LiP·

Finally, the following theorem demonstrates that the i-stable expansions of a formula a correspond precisely to the different i-epistemic states of agent i who only­ knows a.

Theorem 8 Only-Knowing and i-Stable Expansions Let a be basic and wE We with r ={basic a I wpL;a}. Then wpO;a iff r is an i-stable expansion of {a}.

An analogous result was obtained by Halpern [Hal93] .

Corollary 4.1 Basic i-objective foNnulas have a unique i-stable expansion.

5 Conclusion

We proposed a multi-agent logic of only-knowing that extends earlier work by Levesque regarding the single­ agent case. Our logic gives a semantic and proof theo­ retic account of autoepistemic reasoning for many know­ ers. Notions like stable set and stable expansion fall out as natural extensions of single-agent autoepistemic logic.

As for future work, it would be interesting to ob­ tain a complete axiomatization for all of OL. Also, as noted earlier, there are subtle differences between OLn and Halpern's logic. Halpern showed that every valid sentence in his logic is also valid in OLn and that the valid sentences of both logics coincide when restricted to ON c;;. However, there are sentences such as ...,Q;...,Oip that are valid in OLn but not in Halpern's case. For a better com.parison of the two approaches it would be interesting to see which modifications are necessary to obtain identical logics. Finally, a more expressive first­ order language should be considered to make OLn more applicable in real world domains. We conjecture that an approach as in [Lev90] could be adapted for this purpose without great difficulty.

Acknowledgements

I would like to thank Joe Halpern and Hector Levesque for fruitful discussions on this subject .