Query Evaluation and Progression in AOL Knowledge Bases

1 Introduction

A knowledge-based agent in a dynamic environment needs powerful facilities to query its knowledge base. In par­ ticular, it does not suffice to only ask what the world is like after any number of actions have occurred. As has been argued both in the case of static knowledge bases [6; 9] and in the context of reasoning about action [15; 17; 4], the query language should be able to explicitly refer to the agent's knowledge 1 in order to make distinctions such as knowing that versus knowing who [2] which otherwise can­ not be made. This is best illustrated by an example.

Suppose we have a simple, stationary mail sorting robot whose task it is to pick up only the red letters in front of it. Initially the robot has no letters and it is told that there are two letters C and D and that at least one of them is red. (Let us also assume that, unbeknownst to the robot, both letters are red.) Then the robot should be able to answer the following queries:

1. Is there a red letter? Answer: yes.
2. Do you know which one is red? Answer: no.
3. Assume the robot now senses the colour of C. Do you now know of a particular letter that it is red?

1 While we freely use the term knowledge, we really mean belief, but the difference is not important for the purposes of this paper.

Hector J. Levesque

Department of Computer Science University of Toronto Toronto, Ontario Canada M5S 3A6 hector@cs.toronto.edu

Answer: yes. (Note that even if C were not red, the answer would still be yes.)

1. The robot now picks up C. Are you holding all the red letters? Answer: unknown. (For all the robot knows, D could be red or not.)
2. Are you holding all the known red letters? Answer: yes. (Cis the only letter known to be red.)

Recently, Lakemeyer and Levesque [4] have proposed the logic AO£, which amalgamates the situation calculus [14] and Levesque's logic of only-knowing [7) and which has the expressiveness to handle queries such as the above. However, AO£ employs heavy second-order machinery to achieve this and it is not clear how to use the logic in practice other than for specification purposes. In this paper we show that the pic­ ture is not as bleak as it may seem. In particular, we show that in AO£ the evaluation of queries like those in the exam­ ple requires first-order reasoning only.

Another important issue is knowledge base progression. In principle, the only information necessary to answer queries after a number of actions have occurred is the initial knowl­ edge base together with the action sequence and the outcome of sensing actions. However, for long sequences of actions this seems hopelessly unrealistic from a computational point of view. It seems much more sensible to update the knowl­ edge base appropriately after each action has occurred. Lin and Reiter [13] studied progression in the context of the sit­ uation calculus without sensing and epistemic notions. They show that progression can only be represented using second­ order logic in general, but they identify interesting classes of theories where it remains first-order. Here we show how their approach can be applied to the more expressive language of AO £ both at the semantic and the representational level. In particular, we adapt Lin and Reiter's definition of context-free action theories and show that progression remains first-order and efficiently computable in corresponding AO£ knowl­ edge bases.

The rest of the paper is organized as follows. In Section 2, we introduce the logic AO£. In Section 3, we define how to query and progress an agent's knowledge at an abstract level. In Section 4, we consider concrete knowledge bases and dis­ cuss the issue of first-order query evaluation and progression there. The paper ends with some concluding remarks. 2

2 Some preliminary ideas about first-order query processing in

2 The Logic AO .C

Here we only give a brief introduction to the semantics of AO.C. The reader is referred to [4] for a more detailed ac­ count including a characterization using foundational axioms, which we omit here. (We also assume a basic familiarity with the situation calculus.)

The language of AO .C is a dialect of the second-order pred­ icate calculus with equality and has all the primitives of the situation calculus, and some more. There are three sorts of in­ dividuals: ordinary objects, actions, and situations. For each sort there is an infinite supply of variables. The situation vari­ able now is reserved for special use. As in the situation calcu­ lus, we have the following primitives: the constant So denotes the situation which corresponds to the real world before any actions have taken place; if a is an action and s a situation, then do( a, s) denotes the situation resulting from doing a in s; the special predicate Poss( a, s) has the intended meaning that a is executable ins; fluents like Red(x, s) are relations, which have ordinary objects as arguments plus a situation ar­ gument in their final position, and are used to express how the world evolves from situation to situation; there are only finitely many fluents and action function symbols.

We also require two new special predicates, SF( a, s) and K 0 (s), normally not present in the situation calculus, which are used to model sensing and knowledge and will be dis­ cussed in more detail in Section 2.2.

For simplicity, we also make the following restrictions: there are no constants or functions of the situation sort other than So and do; action functions do not take situations as ar­ guments; there are no function symbols of type object; and all predicates other than those mentioned above are fluents .

The language also includes a set of so-called standard names N = {#1 , ~ ·. . . }. The intended use of a standard name is to uniquely identify an object across all possible in­ terpretations, which is useful when dealing with concepts like knowing that versus knowing who. Indeed, the semantics as­ sumes a fixed domain of objects and these are isomorphic with the standard names. (See [6; 9] for more details.)

Atomic formulas are obtained in the usual way from the above primitives and formulas are built using the connec­ tives ..., , 1\, and V. Other connectives like :J and 3 will be used as abbreviations in the usual way. We will use the following conventions: let a = al 0 a2 ° 0 0 0 ° an be a se­ quence of actions and sa situation. Then do( a, s) stands for do( an, do( an-I . .. , do( a1 , s) . . . ) ) . t denotes the empty se­ quence and we sometimes write do(t, s) for s. Finally, we use TRUE as an abbreviation for Vx.(x = x) and FALSE for ·TRUE.

2.1 Semantics

Rather than appealing to the standard semantics of FOL, AO.C comes equipped with a nonstandard semantics derived from possible-world semantics [3], in particular, the seman­ tics of the logic 0 .C [7], which was developed to specify static knowledge bases. 3 As in possible-world semantics, the ba­ sic semantic building-block is a world. However, unlike the static case, a world in AO.C determines what is true initially and after any number of actions have occurred. A situation is then interpreted simply as a world w indexed by a sequence of actions a. In particular, every world "starts" with an ini­ tial situation where no actions have occurred yet. Besides the real world, whose initial situation serves as the denotation of S0 , a model in AO.C also features a set of worlds e. As in modal logics of knowledge like O.C, e should be understood as the set of worlds which the agent considers epistemically possible. In Section 2.2, we will see how, using the special predicate Ko, the worlds in e can be accessed and how this gives us a way to define knowledge in dynamic domains.

AO£ first appeared in [5] . Progression was not handled at all in that paper.

To simplify the semantics, we assume that besides the stan­ dard names for objects there are also standard names for ac­ tions. These are terms of the form A(n1 , . . . , nk) where A is an action function and each ni is a standard name of an object. A primitive formula is an atom of the form F(n1 , ... , nk) where each ni is a standard name, and F ( x1 , ... , x k, s) is a relational fluent, or of the form Poss(A) or SF( A), where A is a standard name for an action. The set of all primitive formulas is P.

Let Act* be the set of all sequences of standard names for actions including the empty sequence t.

Definition 2.1: A world w is a function:

Let W denote the set of all worlds.

Definition 2.2: A situation is a pair (w, a), where w E W and a E Act*. An initial situation is one where a = t.

Definition 2.3: An action model M is a pair (e, w), where wE Wand e ~ W.

w is taken to specify the actual world, and e specifies the epis­ temic state as those worlds an agent has not yet ruled out as being the actual one. As we will see below, a situation term s will be interpreted semantically as a situation ( w, a), consist­ ing of a world and a sequence of actions that have happened so far. A fluent p( s) will be considered true if w [p, a] = 1.

A variable map v is a function that maps object, action, and situation variables into standard names for objects and ac­ tions, and into situations, respectively. In addition, v assigns relations of the appropriate type 4 to relational variables. For a given v, v~ denotes the variable map which is like v except that x is mapped into o.

The meaning of terms

We write I · IM,v for the denotation of terms with respect to an action model M = (e, w) and a variable map v. Then

3 The reader who prefers classical logic is referred to [4], where we provide a second-order axiomatization which is sound and com­ plete with respect to the nonstandard semantics.

4 Since the type will always be obvious from the context, we leave this information implicit.

lxiM,v = v(x), where xis any variable, including pred­ icate variables.

Observe that in a model M = (e, w), the only way to refer to a situation that does not use the given world w is to use a situation variable.

The meaning of formulas

We write M, v f= a to mean formula a comes out true in action model M and variable map v:

sort (object, action, situation, relation).

If a does not mention Ko, that is, the truth of a does not depend on e, we also write w, v f= a instead of M, v f= a. Similarly, if a does not mention S0 and, hence, does not depend on the real world, we write e, v f= a. If a mentions neither S0 nor K0 , we simply write v f= a. Also, if a is a sentence, we omit the variable map and write, for example, Mf=a.

Finally, a formula a is valid in AO.C if for all action mod­ els M = (e, w) and variable maps v, M, v f= a.

2.2 Knowledge and Action

To determine what is known initially (that is, in situation S0), we only need to consider K0 . More precisely, a sentence is known initially just in case it holds in all situations 8 for which K0(8) holds. To find out what holds in successor situ­ ations, we use the predicates SF and Poss. First note that the logic itself imposes no constraints on either SF or Poss; it is up to the user in an application to write appropriate axioms. For Poss, these are the precondition axioms, which specify necessary and sufficient conditions under which an action is executable. So we might have, for example,

as a way of saying that the robot is able to pick up only letters. For SF, the user must write sensed fluent axioms, one for each action type, as discussed in [8]. The idea is that· SF( A, 8) gives the condition sensed by action A in situation 8. So we might have, for example,

as a way of saying that the senseRed action in situation 8 tells the robot whether or not x is red. In case the action A has no sensing component (as in simple physical actions, like dropping an object), we require as a convention that the axiom states that SF(A', 8) is identically TRUE. Actions without a sensing component are referred to as ordinary actions.

With these terms, we can now define K(8 1 , 8) as an abbre­ viation for a formula that characterizes when a situation 8 1 is accessible from an arbitrary situation 8: 5

where the ellipsis stands for the conjunction of

If 8 is an initial situation, then the situations which are K­ related to 8 are precisely those initial situations 8 1 for which K 0(8 1 ) holds. The general picture, after some actions have occurred, is best reflected by the following theorem, which shows that our definition yields the successor state axiom for a predicate K proposed in [J 7] as a solution to the frame problem for knowledge. 6

Theorem 2.4: { 4 }. The following sentence is valid:

In other words, 8 1 is K -related to do( a, 8) just in case there is some other 8 11 which is K -related to 8 and from which 8 1 can be reached by doing a. Furthermore s and 8 11 must agree on the values of SF and Poss for action a.

Given K, knowledge can then be defined in a way similar to possible-world semantics [3; 1; 15] as truth in all acces­ sible situations. Knowing is then denoted using the follow­ ing macro, where a may contain the special situation vari­ able now. Let a~ow refer to a with all occurrences of now replaced by 8. Then

Knows( a, s) = Vs'K(s', s) :J a~,ow

where s' is a new variable occurring nowhere else in a.

Note that a itself may contain Knows with the un­ derstanding that macro expansion works from the inner­ most occurrence of Knows to the outside. For example, Knows(·Knows(Red(x, now), now), 80 ) stands for

and should be read as "the agent knows in S0 that it does not know that x is red."

5 We could have defined K as a predicate in the language as is usually done, but we have chosen not to in order to keep the formal apparatus as small as possible.

6 Here we follow the notation from [8].

3 Queries and Progression

In this section, we will consider two related ways of answer­ ing queries in AO C. For our purposes, a query is any for­ mula with a single free situation variable, now. An example is ::1xRed(x, now) 1\ -.Knows(Red(x, now), now), which asks whether it is now the case that there is a red object which is not known yet. The now in this query is intended to refer to a particular situation, either an initial situation or one that is the result of a sequence of actions. With this view, it is not possible to answer queries wrt an action model M = (e, w) alone, since we also need to specify what sequence of actions to use.

In our first specification of query answering, we are given an initial M, and a sequence of actions a, and we answer according to what would be known in the situation resulting from doing a. In other words, we answer a query a with yes if according toM, a is known in do(a,S0 ):

Note the difference between Knows( a[ now], do( a, S0 )) as above, and Knows(a[do(a, now)], S0 ). In the former, we are asking if a would be known after doing a; in the latter, we are asking if it is known initially that a would be true after doing a. It is not hard to show that the former is implied by the latter, but not vice-versa.

While this is a simple form of query answering, note that it needs to use the world w in M to decide what is known. If a consists of a single sensing action like senseRed(C), then after doing the sensing, the agent should know whether C is red or not. But which one is known is determined by w, which specifies (via SF) how sensing will tum out.

There is, however, a different view where we only need the epistemic state e to answer a query. The idea is that while an agent performs her actions, her epistemic state gets updated to reflect the changes caused by those actions. In particular, a sensing action leads to the removal of worlds which con­ tradict the sensed value. We can define SUCC[e, w, a] to be the epistemic state that results from executing a starting with initial state e with sensing as specified by w, by the following:

Now given an e that is equal to SUCC[e0 , wo, ii], we can de­ fine a new query operation for any query a which does not mention So:

Restricting ourselves to queries that do not mention So is necessary since ASK does not carry with it the real world, which is needed as the denotation of S0 . In fact, mentioning So within a query does not make much sense in the first place.

Consider, for example, a = P(S0 ). Asking whether a is true is completely independent of any epistemic state e and depends only on the initial state of the real world.

In order to compare our two notions of ASK, it is necessary to restrict the class of queries even further. In fact, we restrict ourselves to queries whose only situation term is now. In particular, this has the effect that we cannot ask about other past or future situations.

Definition 3.1: The interaction language IC.

Atomic formulas whose only situation term is now are IC­ formulas. If a and f3 are I£-formulas, then -.a, a 1\ (3, Vxa, where x is an object variable, and Knows(a, now) are IC­ formulas. Nothing else is an IC-formula. From now on, un­ less stated otherwise, a query is an I£-formula where now is the only free variable.

An example query in IC is

The formula

on the other hand, is not in IC.

The formulas of IC are interpreted by first converting them into AOC-formulas using the definition of Knows introduced in the previous section.

We then have the following relationship between ASKo and ASK:

The theorem can be strengthened considerably as it holds for many queries outside of IC as well. In a nutshell, the only restriction needed is that a query does not refer to what is known before the actions a have occurred. Roughly, this is because SUCC[e, w, a] knows more about the past thane be­ cause it has fewer worlds than e. However, the formulation of a broader class of queries for which the theorem holds turns out to be somewhat awkward. IC, on the other hand, is sim­ ple and intuitive. Moreover, it is IC for which we develop a first-order query evaluatioQ method in Section 4.2.

3.1 Progression

For ASK to make sense, we needed to assume that e reflected the epistemic changes that occurred during the execution of a, as reflected in SUCC. In a different context, Lin and Reiter (LR) [13] have called the process of updating a knowledge base of an acting agent progression and they studied it in de­ tail in the framework of the standard situation calculus.

One major difference between progression and the SUCC operation above is that in the former we attempt to forget the history of actions, and treat the resulting knowledge base as if it were an initial one. 7 Indeed, for many applications, it is sufficient to maintain information about a single "current" sit­ uation. Our definition of progression below adapts the ideas of LR to the more expressive language of AOC. In fact, our formulation is somewhat simpler, which is possible because the semantics assumes a fixed set of worlds. It is also more general because LR do not deal with sensing.

7 See [ 12] for a formalization of forgetting.

We can define a progression operator PROG[e, w, a] anal­ ogous to SUCC that produces a new epistemic state, but which loses information about the past. Given worlds w and w', we say that w' agrees with w after a if for all c and p, w'[p, a· CJ = w[p, a· CJ. Note that w and w' may differ ar­ bitrarily in all situations before the last action of a has been performed. Then we define PROG by the following:

1. PROG[e, w, €] = e.

When e = PROG[eo, Wo, a], we say that e is a progression atawrt(eo,wo).

The following theorem states that progression is faithful in that it agrees with the original epistemic state for queries in I£ about what is true after a sequence of actions has oc­ curred.

Theorem 3.3: Let M = (e, w) and Ma = (ea , w), where ea is a progression at a wrt M. Then for all queries a E I£,

Note that in the case of the empty sequence of actions, ASKo[a, M, €] = ASK[a, e, €] follows immediately.

4 AO £ Knowledge Bases

So far, we have only talked about the agent's knowledge in the abstract, namely as a set of worlds, which include all pos­ sible ways they could evolve in the future. Let us now tum to representing the agent's knowledge symbolically and see how this connects with the semantic view taken so far.

In the situation calculus an application domain is typically characterized by the following types of axioms: action pre­ condition axioms, successor state axioms, and axioms de­ scribing the current (often initial) situation. Successor state axioms were proposed by Reiter as a solution to the frame problem [16]. When there are sensing actions, there is also a fourth type called sensed fluent axioms specifying what the outcome of sensing is.

AO£-knowledge bases, as we envisage them, consist of formulas of these types and they have a special syntactic form. We call a formula objective if it does not mention the predicate K o.

A formula ¢ is called simple in t 5 if ¢ is first-order and objective, ts is the only situation argument occurring in any of the predicates, and any variable in t5 occurs only free in a. (:lx.Red(x, do(A, s)) is simple in do(A, s), whereas :ls, x.Red(x, do( A, s)) is not.)

In the following, let A be an action and F a fluent. Let ¢( u) denote a formula whose free variables are among the variables in u.

Lets ::5 s' denote that situations' is a successor of s, which is defined as:

with the ellipsis standing for the conjunction of

Action Precondition Axioms:

\fs\fx.now ::5 s::) [Poss(A(x), s) = ¢(x, s)], 8 where <P(x, s) is simple ins.

Sensed Fluent Axioms:

\fs\lx.now:::; s::) [SF(A(x), s) = ¢(x, s)] where ¢(x, s) is simple ins.

Successor State Axioms:

\fs\fa\lx.now ::5 s::) [Poss(a,s) ::) [F(x,do(a,s)) ¢(x, a, s)JJ, where <P(x, a, s) is simple ins.

Current State Axioms:

¢, where <P is simple in do( a, now) .

A knowledge base (at ii) is then a collection of formulas

where KBp055 , KBsp, and KB65 contain the action pre­ conditions, sensed fuent axioms, and successor state axioms, respectively, and KBcur is the set of current state axioms for a fixed a. A knowledge base at € is called an initial knowledge base.

We define the epistemic state corresponding to a KB as the set of all worlds satisfying the formulas in KB, where now is interpreted by initial situations. Formally,

Defining the epistemic state this way reflects the intuition that the KB is all the agent knows, hence she cannot rule out any world compatible with the sentences in KB. (See [4] for how to formalize "all I know" in AO£.)

4.1 An Example KB

Here we consider the mail-sorting robot example in more de­ tail. There are letters of different colours laid out in front of the robot and its task is to pick up only the red letters. To keep matters simple, there are only two actions, pickup(x), which is possible if x is a letter, and senseRed( x), which tells the robot whether the sensed object is red and which is always possible. There are three fluents, Letter, Red, and HoldRLs. Letter and Red never change and HoldRLs(x, s) is true if the robot is holding the red letter x in situation s.

We can formalize this by defining appropriate precondition axioms, sensed fluent axioms and successor state axioms, all parameterized by now.

Let ALL( now) stand for the set of these formulas:

8 In the situation calculus without epistemic concepts, s ranges over all situations, namely those reachable from So. Here we need to relativize quantification wrt now because there are initial situations other than So.

't/s, x.now ::S s :) Poss(pickup(x), s) = Letter(x, s) 't/s, x .now ::S s :) Poss(senseRed(x), s) =TRUE 't/s, x.now ::S s:) SF(pickup(x), s) =TRUE 't/s, x.now ::S s:) SF(senseRed(x), s) = Red(x, s) 't/s, a, x.now ::S s :) Letter(x , do( a, s)) = Letter(x, s) 't/s,a,x.now ::S s:) Red(x,do(a, s )) = Red(x,s) 't/s,a,x.now ::S s:) HoldRLs(x,do(a,s)) = [(a= pickup(x) 1\ Red(x, s)) V HoldRLs(x , s)]

Initially, the robot knows that there are at least two letters C and D and that one of them is red. Hence let

Let KB =ALL( now) U KBcur ·

Let the real world w be any world such that w f= ALL( now) s~w /\Letter( C, So) /\Red( C, So) 1\Letter(D, So) 1\ Red(D, S0 ), that is, the actions indeed behave as the robot ex­ pects them to and there are at least two red letters C and D. Finally, let M = (~[KB] , w) be our action model.

4.2 First-Order Query Evaluation

By lifting results from Levesque [6; 9], we show that answer­ ing epistemic queries for KB's like the above requires only first-order reasoning.

For any formula a simple in do( a, now) let a!. be a with all occurrences of do( a, now) removed. For example, Red( C, now).!.= Red( C). Let Su denote the set of sentences expressing the unique names assumption for standard names and actions, and let FFoL denote classical first-order logical implication.

The following definition of RES[¢>, KB] shows how to compute in FOL the known instances of¢> and representing it as a first-order equality expression.

Definition 4.1: Let KB = KBcur U KBp088 U KBsF U KBss and ¢> an objective query and let n 1, ... , nk be all the standard names occurring in KB and ¢> and let n' be a name not occurring in KB or ¢>. Then RES[¢>, KB] is defined as:

1. If ¢1.. has no free variables, then RES[¢>, KB] is TRUE, if KBc117-l. USu F FoL ¢!.., and FALSE, otherwise.

If we consider our example KB, then RES[Letter(x , now)] reduces (after simplification) to (x =C) V (x = D) whereas RES[Red(x, now)] reduces to FALSE because there are no known red things. The next definition applies RES to all occurrences of Knows within a query using a recursive de­ scent denoted by II · ~KB· The idea is that any occurrence of Knows(a, now) in a query is replaced by an equality expres­ sion describing the known instances of a.

Definition 4.2:

Given a KB as defined above and an arbitrary query a, II a IlKs is the objective formula simple in now defined by

~aiiKs = a, when a is objective; 11-,aiiKB = 'II a IlKs; ll(a 1\ ,B) IlKs = (llaiiKs 1\ II.BI!Ks); IIVxaiiKB = VxllaiiKs;

IIKnows(a,nowHKB = RES[IIaiiKs , KB] .

Theorem 4.3: Let KB be a knowledge base at a with current state axioms KBcur· Then ASK[a, ~[KB], a] =yes iff

In essence, the theorem says that answering an epistemic query can be achieved by computing a finite number of first­ order implications. Restricting ourselves to queries in I£ is essential in this case.

To illustrate what this theorem says consider the ex­ ample KB and the query a 3xRed(x,now) 1\ -,Knows(Red(x, now)). Then ASK[a, ~[KB], now] = yes because of the following: RES[Red(x, now), KB] simplifies to FALSE because there are no known instances of red ob­ jects. Hence llaiiKs..l. is equivalent to 3xRed(x) 1\ -,fALSE and, furthermore, KBcur..l. USu F FOL 3xRed(x).

Being able to reduce query evaluation in AOC to first­ order reasoning under certain restrictions is somewhat analo­ gous to a result by Lin and Reiter [13] for the standard (non­ epistemic) situation calculus. They show that, even though their foundational axioms for the situation calculus include a second-order axiom to characterize the set of all situations, this axiom is not needed when doing temporal projection, that is, when inferring whether a formula¢> simple in do( a, S0 ) follows from the domain theory together with the founda­ tional axioms. There are also other examples such as [11] which show that theories which are inherently second-order nevertheless have interesting special cases where first-order reasoning alone suffices.

4.3 Context-Free Knowledge Bases

Lin and Reiter showed that in their framework, progression is not always first-order definable. We conjecture that the same is true in AOC, but just as in LR's case there are interesting classes of knowledge bases which are not only first-order representable but where progression is also easily computable. LR discuss in particular the classes they call relatively-complete and context-free action theories. Here we adapt and extend context-free action theories for AOC and obtain very similar results. (The same is true for relatively complete theories, but we omit them for space reasons.)

A fluent F is called situation independent if its successor state axiom has the form 't/s't/a't/i.now ::S s :) [Poss(a, s) :) [F(i,do(a, s)) = F(i,s)]] , that is, F never changes. Oth­ erwise F is called situation dependent. A formula is called situation independent if it contains only situation independent ftuenb. ·

Definition 4.4: [Lin and Reiter] A KB is context-free if

• KB ·· consists of successor state axioms of the form 't/s't/a't/i.now ::S s :) [Poss(a,s) :) [F(i,do(a,s)) = 'Yt(x,a,s) v (F(i,s) 1\ ''Y.F(i,a,s))]], where 'Yt(x, a, s) and 'Y.F(i, a, s) are situation independent. 9

9 The idea is that rt describes the conditions which cause F to be true and ri- those which cause it to be false.

• KBcur consists of situation independent formulas and formulas of the form Vx.'lj; :> F(x,do(a, now)) or Vx.'lj; :> ·F(x,do(a, now)), where 'ljJ is a situation in­ dependent formula with free variables in x and now.
• For every action precondition axiom Vs'Vx.now ::5 s :> [Poss(A(x) , s) = ¢>(x, s)], ¢>(x, s) is situation independent.
• For every sensed fluent axiom Vs'Vx.now ::5 s :> [SF(A(x), s) = 'lj;(x, s)], 'lj;(x, s) is situation independent.

The conditions on the sensed fluent and action precondition axioms are missing in LR's definition because they do not deal with sensing and they do not consider the case where an agent successfully performs an action even though she does not know that it is possible. In a sense, finding out that an ac­ tion is possible by doing it can be thought of as a special form of sensing. Note also that SF and Poss are treated completely symmetricly in our semantic definition of progression.

Definition 4.5: Let KB = KBcur U KBPoss U KBsF U KBss be a context-free knowledge base at a, Wo a world, A = Act( n) an action, and let S! = do( a, now) and Sz = do( a· A, now). Let the action precondition and sensed fluent axioms for A be

Then let KBA = KB:ur U KBp0 88 U KBsF U KBss· where KB:uris constructed as follows:

1. Let A be a sensing action. Then:
2. -If¢> E KBcur then¢>~~ E KB:ur;
3. -if wo f= Poss(A, do( a, So)) then ¢>A (n, sz) E KB:ur else ·¢>A(n,sz) E KB:ur;
4. -if wo f= SF( A, do( a, So)) then '1/JA (n, sz) E KB:ur else·'I/JA(n,sz) E KB:ur·
5. Let A be an ordinary action. Then:
6. -If¢> E KBcur is sit. independent, then ¢>~~ E KB:ur;
7. -for any situation dependent fluent F add to KB:ur Vx.,j.(x, A, sz) :> F(x, sz) and Vx.Yi (x, A, Sz) :> ·F(x, sz);
8. If'Vx.'lj; :> F(x, si) is in KBcur. then add Vx.'l/J!~ 1\ 'rp (x, A, sz) :> F(x, sz);
9. lf'Vx.'lj; :> ·F(x, si) is in KBcur· then add Vx.'l/J;~ A .,j.(x, A, sz) :> ·F(x, sz));
10. -if wo f= Poss(A, do(a, So)) then ¢>A (n, sz) E KB:ur else ·¢>A(n, sz) E KB:ur·

Note the different treatment depending on whether A is a sensing action or not. In the former case, the old contents of KBcur is simply copied to the new knowledge base with the new situation s2 replacing the old s1 . If A is an ordi­ nary action, we need to treat the situation dependent fluents in KBcur in a special way in order to reflect the changes that result from doing A. In the case of a sensing action we also need to record the values of ¢>A and '1/JA depending on the truth value of Poss(A) and SF( A) at (w0 , a). If A is an or­ dinary action, this needs to be done only for ¢>A because we assume that 'ljJ A is equivalent to TRUE for ordinary actions.

It is not hard to see that the property of being context-free is preserved by our syntactic form of progression.

Lemma 4.6: Let KB, KBA, and A be as in Definition 4.5. Then KBA is context-free.

In their paper [13], LR describe some very simple (and reasonable) consistency requirements for context-free knowl­ edge bases. 10 We will not repeat those conditions here and simply refer to them as LR-consistency. We are now ready to show that syntactic progression of context-free KB's con­ forms with our semantic definition.

Theorem 4.7: Let KB0 be an initial knowledge base, w0 a world and e0 = ~[KB0 ]. Let KB, KBA and A be as in Defi­ nition 4.5 such that ~[KB] is a progression at a wrt (e0 , w0 ).

if KB is LR-consistent, then ~[KBA] is a progression of ~[KB] at a wrt (eo, wo).

Note that, by definition, KB0 is itself a progression at E wrt (e0 , w0 ). Hence, the theorem tells us that, starting in an initial context-free knowledge base, doing an action A will lead to a progression which itself is represented by a context­ free knowledge base, and this process iterates.

To illustrate how progression works, let us consider the initial KB and the corresponding action model M = (~[KB] , w) from Section 4.1. First, it is easy to verify that it conforms to the definition of a context-free KB.

1. Let us consider progressing KB by A = sense Red( C) resulting in KBA with corresponding KBA. Let s1 stand for do( sense Red( C) , now).

Since A is a sensing action (case (1) of Def. 4.5), we ob­ tain KB:ur simply by replacing every occurrence of now in KBcur by s1 and adding Red( C, s1 ) to it, because we assume that M f= SF(senseRed(C), S0 ). Then ~[KBA] is a pro­ gression at A.

Let o: = 3xRed(x, now) 1\ Knows(Red(x, now) , now). Then ASK[o:, ~[KBA], A] = yes because now there is a known red letter, namely C.

2. Let us now progress KBA by A' = pickup(C) result­ ing in KBAA' with corresponding KB:u~'. Let s2 stand for do(pickup( C), si).

Starting with the empty set we construct KB:u~' by adding the following sentences: 11

• Letter( C, s2 ) , Letter(D, sz), Red( C, Sz)

(The disjunction (Red(C, s2 ) V Red(D, sz)) is omitted be­ cause it is clearly subsumed by Red( C, sz) .)

Given the successor state axiom for F = HoldRLs, we obtain

r F = FALSE and r't(x, A, s2 ) = [pickup(C) = pickup(x) 1\Red(x,sz)] .

10 0ne such requirement is that rt and I"F may never be true simultaneously. The example KB is LR-consistent.

11 For simplicity, we omit adding sentences that tum out to be valid or subsumed by others.

Hence we add

• -Vx.''(j.(x, A, 82) => HoldRLs(x, 8 2 )

Finally, the last case of Definition 4.5 applies and we add

• Vx.-."Yt(x , A, 82) => -.HoldRLs(x, 82 )

Given the unique names assumption for standard names of objects and actions, "Y t ( x, A, 8 2 ) is true just in case x = C, that is, the agent is holding precisely C in 8 2 .

Given this progressed knowledge base it is then not hard to show that the robot does not know in 8 2 whether it is holding all the red letters. Formally, let

• a= Vx.Red(x, now) 1\ Letter(x, now)=> Knows(Red(x , now) 1\ Letter(x, now), now).

Then ASK[ a, ~[KBAA'], A · A'] = unknown. This is be­ cause there are worlds in ~[KBAA'] where C is the only red letter and others where there are red letters other than C after doing A· A'.

5 Conclusions

Using the second-order logic AO.C, we specified a query fa­ cility for knowledge bases in dynamic worlds. Despite the expressiveness of the logic, we showed that query evaluation often requires only first-order reasoning. Moreover, by adapt­ ing and extending results by Lin and Reiter, we gave a seman­ tic definition of progression and showed that it is first-order representable in the case of context-free knowledge bases.

Future work includes finding more powerful classes of knowledge bases with first-order progressions and applying the results to the action programming language GOLOG [10]. We defined progression in a way that is very close to the orig­ inal definition by Lin and Reiter. The exact relationship be­ tween the two still needs to be determined. Also, our earlier definition of SUCC can be thought of as a progression op­ erator in its own right. It is more powerful in that nothing about the past is forgotten. It is an interesting open problem to determine syntactic variants of this notion of progression.