A Semantical Account of Progression in the Presence of Defaults

1 Introduction

In previous work, Lakemeyer and Levesque [2004; 2005] proposed a modal fragment of the situation calculus called ES, which fully captures Reiter's basic action theories and regression-based reasoning, including reasoning about knowledge. So, for example, the language allows us to formulate Reiter-style successor state axioms such as this one:

In English: after any sequence of actions (□), an object x will be broken after doing action a ([a]Broken(x)) iff a is the dropping of x when x is fragile, or x was already broken and a is not the action of repairing it. Here we assume that Fragile is a predicate which is not affected by any action so that its successor state axiom would be

Let us call the conjunction of these two axioms SSABF . In addition to action and change, the language ES also addresses what an agent knows and only-knows. The latter is intended

Hector J. Levesque

Dept. of Computer Science University of Toronto Toronto, Ontario Canada M5S 3A6

hector@cs.toronto.edu

to capture all an agent knows in the sense of having a knowledge base. For illustration, consider the following sentence, which is logically valid in ES:

In English: if all the agent knows is that o is fragile and not broken and that the successor state axioms for Broken and Fragile hold, then after dropping o, the agent knows that o is broken, but does not know that o is made of glass.

Let us now consider what the agent should only-know after the drop action has occurred. Intuitively, the agent's knowledge should change in that it now believes that o is broken, with everything else remaining the same. Formally,

In fact this view corresponds essentially to what Lin and Reiter (LR) [1997] call the progression of a database wrt an action. It turns out, however, that the semantics of onlyknowing as proposed in [Lakemeyer and Levesque, 2004] differs from this in that the last formula above is not entailed. The reason is that their version, unlike progression, does not forget what was true initially (like whether or not o was already broken), and so more ends up being known.

The LR notion of progression allows for efficient implementations under certain restrictions [Lin and Reiter, 1997; Liu and Levesque, 2005; Vassos and Levesque, 2007], and being able to forget the past seems essential for this. Hence the previous semantics of only-knowing may not be very useful, except perhaps in the initial state. In this paper, we present a new semantics of only-knowing which avoids this pitfall and is fully compatible with LR's idea of progression.

Levesque [1990] showed that only-knowing in the static case also accounts for default reasoning in the sense of autoepistemic logic [Moore, 1985]. For example, the default that objects are fragile unless known otherwise can be written as

If the agent uses this default instead of the fact that o is fragile then it would still conclude, this time by default, that o is fragile and hence believe that it is broken after dropping it. But suppose that o is actually not fragile. What should the agent believe after sensing the status of o's fragility? Clearly, it should then believe that o is indeed not fragile and it should not believe that dropping o will break it. That is, the default should no longer apply. Unfortunately, the previous definition of only-knowing does not do this. The problem, roughly, is that the initial default conclusion that o is fragile cannot be distinguished from a hard fact. Subsequently sensing the opposite then leads to an inconsistency.

In this paper we will fix this problem by proposing a semantics which separates conclusions based on facts from those based on defaults. To this end, we will distinguish between what is known for sure (using the modality K) and what is believed after applying defaults (using another modality B). In fact, defaults themselves will be formulated using B instead of K. All this will be integrated with progression in the sense that defaults will be applied to the progressed knowledge base.

For space reasons, the paper contains no proofs. These and a comparison between the old and new semantics of onlyknowing and between our notion of progression and that of LR can be found in [Lakemeyer and Levesque, 2009].

The rest of the paper is organized as follows. In the next section, we introduce the logic ESO, which is like the old ES except for the new semantics of only-knowing and defaults. This semantics agrees with the previous one in the static case. After that, we consider only-knowing in the context of basic action theories. In particular, we show that what is onlyknown after an action extends LR's original idea of progression, and how reasoning about defaults fits into the picture. We then address related work and conclude.

2 The Logic ESO

The language is a second-order modal dialect with equality and sorts of type object and action. Before presenting the formal details, here are the main features:

• rigid terms: The ground terms of the language are taken to be isomorphic to the domain of discourse. This allows first-order quantification to be understood substitutionally. Equality can also be given a very simple treatment: two ground terms are equal only if they are identical.
• knowledge and truth: The language includes modal operators K and B for knowledge and belief. The K operator allows us to distinguish between sentences that are true and sentences that are known (by some implicit agent). The B operator allows an agent to have false beliefs about its world or how its world changes. For example, we can model situations where an object is not fragile but the agent does not know it, yet may believe that it is fragile by default.
• sensing: The connection between knowledge and truth is made with sensing. Every action is assumed to have a binary sensing result and after performing the action, the agent learns that the action was possible (as indicated by the Poss predicate) and whether the sensing result for the action was 1 or 0 (as indicated by the SF predicate). 1 Just as an action theory may contain precon-

1 For convenience, we assume that every action returns a (perhaps trivial) sensing result. Here, we restrict ourselves to binary values. See [Scherl and Levesque, 2003] for how to handle arbitrary sensing

dition axioms characterizing the conditions under which Poss holds, it can contain axioms characterizing the conditions under which SF holds.

2.1 The language

The symbols of ESO consist of first-order variables, secondorder predicate variables of every arity, rigid functions of every arity, fluent predicate symbols of every arity, as well as these connectives and other symbols: =, ∧, ¬, ∀, K, B, O, Ω, □, round and square parentheses, period, comma. We assume two special fluent predicates Poss and SF (for sensing). K, B, O, and Ωare called epistemic operators.

The terms of the language are formed in the usual way from first-order variable and rigid functions.

We let R denote the set of all rigid terms (here, all ground terms). For simplicity, instead of having variables of the action sort distinct from those of the object sort as in the situation calculus, we lump both of these together and allow ourselves to use any term as an action or as an object. 2

The well-formed formulas of the language form the least set such that

1. If t1, . . . , tk are terms, F is a k-ary predicate symbol, and V is a k-ary second-order variable, then F(t1, . . . , tk) and V (t1, . . . , tk) are (atomic) formulas;
2. If t1 and t2 are terms, then (t1 = t2) is a formula;
3. If α and β are formulas, v is a first-order variable, V is a second-order variable, and t is a term, then the following are also formulas: (α∧β), ¬α, ∀v. α, ∀V. α, [t]α, □α, Kα, Bα, Oα, and Ωα, where the formulas following O and Ωare restricted further below.

We read [t]α as "α holds after action t", and □α as "α holds after any sequence of actions," and Kα (Bα) as "the agent knows (believes) α." Oα may be read as "the agent only-knows α" and is intended to capture all the agent knows about what the world is like now and how it evolves as a result of actions. Here no defaults are taken into account, just facts which, as we will see later, come in the form of a basic action theory similar to those proposed by Reiter [2001a]. Therefore, we restrict O to apply to so-called objective formulas only, which are those mentioning no epistemic operators. Finally, Ωα is meant to capture all and only the defaults believed by the agent. For that, α is restricted to what we call static belief formulas, which mention neither □ nor [t] nor any epistemic operator except B.

As usual, we treat (α∨β), (α ⊃ β), (α ≡ β), ∃v. α, and ∃V. α as abbreviations. We use αxt to mean formula α with all free occurrences of variable x replaced by term t. We call a formula without free variables a sentence.

We will also sometimes refer to static objective formulas, which are the objective formulas among the static belief formulas, and fluent formulas, which are formulas with no K, O, B, Ω, □, [t], Poss, or SF. 3

results.

2 Equivalently, the version in this paper can be thought of as having action terms but no object terms.

3 In the situation calculus, these correspond to formulas that are uniform in some situation term.

2.2 The semantics

The main purpose of the semantics we are about to present is to be precise about how we handle fluents, which may vary as the result of actions and whose values may be unknown. Intuitively, to determine whether or not a sentence α is true after a sequence of actions z has been performed, we need to specify two things: a world w and an epistemic state e. A world determines truth values for the ground atoms after any sequence of actions. An epistemic state is defined by a set of worlds, as in possible-world semantics.

More precisely, let Z be the set of all finite sequences of elements of R including 〈 〉, the empty sequence. Z should be understood as the set of all finite sequences of actions. Then

• a world w ∈ W is any function from G (the set of ground atoms) and Z to {0, 1}.
• an epistemic state e ⊆ W is any set of worlds.

To interpret formulas with free variables, we proceed as follows. First-order variables are handled substitutionally using the rigid terms R. To handle the quantification over second-order variables, we use second-order variable maps defined as follows:

The second-order ground atoms are formulas of the form V (t1, . . . , tk) where V is a second-order variable and all of the ti are in R. A variable map u is a function from second-order ground atoms to {0, 1}.

Let u and u′ be variable maps, and let V be a second-order variable; we write u′ ∼V u to mean that u and u′ agree except perhaps on the assignments involving V .

Finally, to interpret what is known after a sequence of actions has taken place, we define w′ ≃z w (read: w′ agrees with w on the sensing throughout action sequence z) inductively by the following:

Note that ≃z is not quite an equivalence relation because of the use of Poss here. This is because we are insisting that the agent comes to believe that Poss was true after performing an action, even in those "non-legal" situations where the action was not possible in reality. 4

Putting all these together, we now turn to the semantic definitions for sentences of ESO. Given an epistemic state e ⊆ W, a world w ∈ W, an action sequence z ∈ Z, and a secondorder variable map u, we have:

1. e,w, z, u |= V (t1, . . . , tk) iff u[V (t1, . . . , tk)] = 1;

1. e,w, z, u |= (α∧ β) iff e, w, z, u |= α and e, w, z, u |= β;

4 An alternate account that would state that the agent learns the true value of Poss (analogous to SF) is a bit more cumbersome, but would allow≃z to be a full equivalence relation.

To define the meaning of the epistemic operators, we need the following definition:

Definition 1 Let w be a world and e a set of worlds, and z a sequence of actions. Then

1. wz is a world such that wz[p, z ′ ] = w[p, z · z ′ ] for all ground atoms p and action sequences z ′ ;

Note that wz is exactly like w after the actions z have occurred. So in a sense, wz can be thought of as the progression of w wrt z. ewz then contains all those worlds of e which are progressed wrt z and which are compatible with (the real) world w in terms of the sensing results and where all the actions in z are executable. Note that when z is empty, ewz = e.

In other words, knowing α in e and w after actions z means that α is true in all the progressed worlds of e which are compatible with w. Oα is quite similar except for the "iff," whose effect is that ewz must contain every world which satisfies α.

B and Ωare meant to capture what the agent believes in addition by applying defaults. Having more beliefs (as a result of defaults) is modeled by considering a subset of the worlds in ewz . For that purpose, we introduce a function δ which maps each set of worlds into a subset. In particular, we require that δ(ewz ) ⊆ ewz . As δ is now part of the model (just like w and e) we add it to the L.H.S. of the satisfaction relation with the understanding that the previous rules are retrofitted with δ as well. Then we have:

Note that the only difference between K and B is that the latter considers δ(ewz ) instead of ewz . Likewise, the definition of Ω is similar to that of O. The role of Ω is to constrain δ to produce a special subset of ewz . Roughly, the effect of the definition of Ωα is that one starts with whatever facts are believed (represented by ewz ) and then settles on a largest subset of ewz such that α (representing the defaults) is also believed.

We say that a sentence in ESO is true at a given e, w, and δ (written e,w, δ |= α) if e,w, 〈 〉, u, δ |= α for any secondorder variable map u. If Σ is a set of sentences and α is a sentence, we write Σ |= α (read: Σ logically entails α) to mean that for every e, w, and δ, if e,w, δ |= α′ for every α′ ∈ Σ, then e, w, δ |= α. Finally, we write |= α (read: α is valid) to mean {} |= α.

For reasons of space we cannot go into details about the general logical properties of the epistemic operators. To demonstrate that the operators are well-behaved, we only list some properties, which all have simple semantic proofs:

Moreover, K and B satisfy the usual K45 axioms of modal logic [Hughes and Cresswell, 1968] and they are mutually introspective, e.g. |= □(Bα ⊃KBα).

3 The Semantics of Progression and Defaults

3.1 Basic action theories

Let us now consider the equivalent of basic action theories of the situation calculus. Since in our logic there is no explicit notion of situations, our basic action theories do not require foundational axioms like Reiter's [2001a] second-order induction axiom for situations. The treatment of defaults is deferred to Section 3.3.

Definition 2 Given a set of fluents F, a set Σ ⊆ ESO of sentences is called a basic action theory over F iff

1. Σ0 is any set of fluent sentences;
2. Σpre is a singleton sentence of the form □Poss(a) ≡ π, where π is a fluent formula; 5
3. Σpost is a set of sentences of the form □[a]F(⃗v) ≡ γF , one for each relational fluent F in F, respectively, and where the γF are fluent formulas. 6
4. Σsense is a sentence exactly parallel to the one for Poss of the form □SF(a) ≡ ϕ, where ϕ is a fluent formula.

The idea here is that Σ0 expresses what is true initially (in the initial situation), Σpre is one large precondition axiom, and Σpost is a set of successor state axioms, one per fluent in F, which incorporate the solution to the frame problem proposed by Reiter [1991]. Σsense characterizes the sensing results of actions. For actions like drop(o), which do not return any useful sensing information, SF can be defined to be vacuously true (see below for an example).

We will usually require that Σpre, Σpost, and Σsense be firstorder. However, Σ0 may contain second-order sentences. As we will see, this is inescapable if we want to capture progression correctly. In the following, we assume that Σ (and hence F) is finite and we will freely use Σ or its subsets as part of sentences with the understanding that we mean the conjunction of the sentences contained in the set.

5 We assume that all free variables are implicitly universally quantified and that □ has lower syntactic precedence than the logical connectives, so that □Poss(a) ≡ π stands for the sentence ∀a.□(Poss(a) ≡ π).

6 The [t] construct has higher precedence than the logical connectives. So □[a]F(⃗x) ≡ γF abbreviates the sentence ∀a, ⃗x.□([a]F(⃗x) ≡ γF ).

3.2 Progression = Only-knowing after an action

Let us now turn to the first main result of this paper. The question we want to answer is this: suppose an agent is given a basic action theory as its initial knowledge base; how do we characterize the agent's knowledge after an action is performed? As hinted in the introduction, only-knowing will give us the answer.

In the following, for a given basic action theory Σ, we sometimes write φ for Σ0 and □β for the rest of the action theory Σpre ∪ Σpost ∪ Σsense. We assume that π and ϕ refer to the right-hand sides of the definitions of Poss and SF in Σ, and γF is the right-hand side of the successor state axiom for fluent F. Also, let ⃗ F consist of all the fluent predicate symbols in Σ, and let ⃗ P be corresponding second-order variables, where each Pi has the same arity as Fi. Then α ⃗ F⃗ P denotes the formula α with every occurrence of Fi replaced by Pi.

The following result characterizes in general terms all that is known after performing an action:

Theorem 1 Let Σ = φ ∧ □β be a basic action theory and t an action term. Then

What the theorem says is that if all the agent knows initially is a basic action theory, then after doing action t all the agent knows is another basic action theory, where the dynamic part (□β) remains the same and the initial database φ is replaced by Ψ or Ψ′ , depending on the outcome of the sensing. Note that the two sentences differ only in one place, ϕat vs. ¬ϕat . Roughly, Ψ and Ψ′ specify how the truth value of each fluent F in F is determined by what was true previously (φ), taking into account that the action was possible (πa t ) and that the sensing result was either true (ϕat ) or false (¬ϕat ). Since after performing an action, the agent again only-knows a basic action theory, we can take this as its new initial theory and the process can iterate. We remark that our notion of progression is very closely related to progression as defined by [Lin and Reiter, 1997], but extends it to handle sensing actions. Note that, while Lin and Reiter need to include the unique names axioms for actions in the progression, we do not, as these are built into the logic.

We mentioned above that after an action, the resulting knowledge base can be taken as the new initial knowledge base, and the progression can iterate. The following theorem shows that this view is justified in that the entailments about the future remain the same when we substitute what is known about the world initially by its progression. Here we only consider the case where SF(t) is true.

In English (roughly): It follows from your initial knowledge base that you will know α after doing action t iff knowing α follows from your progressed knowledge base.

3.3 Defaults for basic action theories

Here we restrict ourselves to static defaults like "birds normally fly." In an autoepistemic setting [Moore, 1985; Levesque, 1990], these have the following form:

which can be read as "if α is believed and β is consistent with what is believed then assume γ." Here the assumption is that α, β, and γ are static objective formulas.

Let Σdef be the conjunction of all defaults of the above form held by an agent. For a given basic action theory Σ, as defined in Section 3.1, the idea is to apply the same defaults to what is known about the current situation after any number of actions have occurred, that is, for the purpose of default reasoning, we assume that □ΩΣdef holds. The following theorem relates what is then believed after one action has occurred (where SF returns true) with stable expansions [Moore, 1985]. 7

Theorem 3 Let t be a ground action and Σ = φ∧□β a basic action theory such that |= OΣ ∧ SF(t) ⊃ [t]O(ψ ∧ □β) and ψ is first order. Then for any static belief sentence γ,

γ is in every stable expansion of ψ ∧ Σdef.

3.4 An example

To illustrate progression, let us consider the example of the introduction with two fluents Broken and Fragile, actions drop(x), repair(x), and senseF(x) (for sensing whether x is fragile). First, we let the basic action theory Σ consist of the following axioms:

• Σ0 = {Fragile(o), ¬Broken(o)};
• Σpre = {□Poss(a) ≡ true} (for simplicity);
• Σpost = {SSABF} (from the introduction);
• Σsense = {□SF(a) ≡ ∃x.a = drop(x) ∧ true ∨ a = repair(x) ∧ true ∨ a = senseF(x) ∧ Fragile(x)}.

As before, let □β be Σpre ∪ Σpost ∪ Σsense. Then we have

Using the fact that all actions are distinct, it is not difficult to see that Ψ can be simplified to

In other words, after dropping o, the agent's knowledge base is as before, except that o is now known to be broken.

To see how defaults work, we now let Σ be as before except that Σ0 = {¬Broken(o)} and let Σ′ = Σ ∪ {¬Fragile(o)}. Let Σdef = {∀x.¬B¬Fragile(x) ⊃ Fragile(x)}. Then the following are logical consequences of

7 Roughly, E is a stable expansion of α iff for all γ, γ ∈ E iff γ is a first-order consequence of {α}∪{Bβ | β ∈ E}∪{¬Bβ | β ̸∈ E}.

1. BFragile(o);
2. [drop(o)]BBroken(o);
3. [senseF(o)]K¬Fragile(o);
4. [senseF(o)][drop(o)]K¬Broken(o).

(1) holds because of the default, since o's non-fragility is not yet known. Notice, in particular, the role of ΩΣdef: while the semantics of ESO puts no restrictions on δ other than δ(e) ⊆ e, 8 it is ΩΣdef which forces δ(e) to be the largest subset of e which is compatible with the default, that is, δ selects only worlds from e where o is fragile. (2) holds because the default also applies after drop(o). In particular, Theorem3 applies as [drop(o)]O(Broken(o) ≡ Fragile(o) ∧ □β) follows as well. Finally, in (3) and (4) the agent has found out that o is not fragile, blocking the default since |= □(Kα ⊃ Bα).

4 RelatedWork

While the situation calculus has received a lot of attention in the reasoning about action community, there are, of course, a number of alternative formalisms, including close relatives like the fluent calculus [Thielscher, 1999] and more distant cousins such as [Kowalski and Sergot, 1986; Gelfond and Lifschitz, 1993].

While ESO is intended to capture a fragment of the situation calculus, it is also related to the work formalizing action and change in the framework of dynamic logic [Harel, 1984]. Examples are [De Giacomo and Lenzerini, 1995] and later [Herzig et al, 2000], who also deal with belief. While these approaches remain propositional, there are also firstorder treatments such as [Demolombe, 2003; Demolombe, Herzig, and Varzinczak, 2003; Blackburn et al, 2001], which, like ESO, are inspired by the desire to capture fragments of the situation calculus in modal logic. Demolombe (2003) even considers a form of only-knowing, which is related to the version of only-knowing in [Lakemeyer and Levesque, 2004], which in turn derives from the logic OL [Levesque and Lakemeyer, 2001].

The idea of progression is not new and lies at the heart of most planning systems, starting with STRIPS [Fikes and Nilsson, 1971], but also in implemented agent programming languages like 3APL [Hindriks et al, 1999]. Lin and Reiter (1997) so far gave the most general account. Restricted forms of LR-progression, which are first-order definable, are discussed in [Lin and Reiter, 1997; Liu and Levesque, 2005; Claßen et al, 2007; Vassos and Levesque, 2007].

Default reasoning has been applied to actions mostly to solve the frame problem [Shanahan, 1993]. Here, however, we use Reiter's monotonic solution to the frame problem [Reiter, 1991] and we are concerned with the static "Tweetyflies" variety of defaults. Kakas et al. [2008] recently made a proposal that deals with these in the presence of actions, but only in a propositional setting of a language related to A [Gelfond and Lifschitz, 1993].

5 Conclusion

The paper introduced a new semantics for the concept of only-knowing within a modal fragment of the situation calculus. In particular, we showed that, provided an agent starts with a basic action theory as its initial knowledge base, then all the agent knows after an action is again a basic action theory. The result is closely related to Lin and Reiter's notion of progression and generalizes it to allow for actions which return sensing results. We also showed how to handle static defaults in the sense that these are applied every time after an action has been performed. Because of the way only-knowing is modelled, defaults behave as in autoepistemic logic. In previous work we showed that by modifying the semantics of only-knowing in the static case, other forms of default reasoning like Reiter's default logic can be captured [Lakemeyer and Levesque, 2006]. We believe that these results will carry over to our dynamic setting as well.

8 Here e is the (unique) set of worlds which satisfies O(Σ0∧□β).