Progression of Situation Calculus Action Theories with Incomplete Information

1 Introduction

This paper deals with the problem of getting a robot or agent to reason efficiently about action and change under the following three conditions:

1. the agent has incomplete knowledge about certain changing values in the world (fluents);
2. the agent has both physical (world-changing) and sensing (knowledge-producing) actions at its disposal;
3. the agent is long-lived and may have performed thousands or even millions of actions to date.

These conditions are typical of robots or agents that must operate autonomously over long periods of time, such as the agents found in role-playing games. For example, an agent may not know the relative locations of other agents or important objects, but may be able to move and to sense what agents and objects are nearby. The challenge is to reason efficiently about the overall state of the world in this setting, taking into account what has been done and what has been sensed, as a large number of such actions are performed.

There is a significant body of work on logical formalisms for dynamic domains that are appropriate here, such as the situation calculus [McCarthy and Hayes, 1969], the event calculus [Kowalski and Sergot, 1986], and the fluent calculus [Thielscher, 1999]. In logical terms, we seek an efficient solution to the projection problem [Reiter, 2001]: given an action theory that specifies the preconditions and effects of actions (including sensing), and a knowledge base about the initial state of the world, determine whether or not some condition holds after a given sequence of actions has been performed. This is a fundamental reasoning problem and a necessary prerequisite to other forms of reasoning in dynamic domains such as planning and high-level program execution. While the projection problem can be solved by regression or by progression [Lin, 2007], it is generally agreed that regression alone is impractical when the number of actions is large [Lakemeyer and Levesque, 2007].

While formalisms based on logic can represent a general form of incomplete knowledge in a straightforward way, they would then require systems based on some form of theoremproving. It is quite typical of the practical implementations of these formalisms to forego this generality and either insist on complete knowledge or to employ an inference mechanism that is logically incomplete. For the situation calculus, the former approach was taken in the practical implementations of the GOLOG agent programming language [Levesque et al., 1997; De Giacomo and Levesque, 1999]; the latter was taken by Liu and Levesque [2005] where incomplete knowledge was dealt with using a logically incomplete form of progression. In the FLUX implementation of the fluent calculus [Thielscher, 2004] incomplete knowledge is dealt with using constraint rules and a logically incomplete constraint solver.

In this paper, we propose a new progression mechanism for a restricted form of incomplete knowledge formulated as a basic action theory in the situation calculus. Specifically, we focus on functional fluents and deal directly with the possible values these fluents may have and how these values are affected by both physical and sensing actions. Our approach handles a restricted form of (functional) local-effect action theories but generalizes the Liu and Levesque account where progression is logically complete only for action theories that are context complete, that is, where there is complete knowledge about the context of any context-dependent successor state axioms. Our method can be calculated efficiently using database techniques (related to those of [Antova et al., 2007]) under certain reasonable assumptions. To our knowledge, no other logical formalism handles progression (and therefore the projection task) in a way that is both logically complete and practical under the three conditions listed above.

The rest of the paper is organized as follows. In Section 2, we review the situation calculus notation, as well as the definitions of projection and progression. In Section 3, we discuss the notion of a possible value and define the localeffect and bounded action theories. In Section 4, we present a progression mechanism for local-effect and bounded theories and in Section 5, we discuss the complexity of the approach. In Section 6, we discuss related work. Finally, in Section 7, we draw conclusions and discuss future work.

2 Situation calculus theories and progression

The situation calculus [McCarthy and Hayes, 1969] is a first-order language with some limited second-order features specifically designed for representing dynamically changing worlds. The language has disjoint sorts for actions, situations, and objects (everything else).

A situation represents a world history as a sequence of actions. The constant S0 is used to denote the initial situation where no actions have been performed. Sequences of actions are built using the function symbol do, such that do(a, s) denotes the successor situation resulting from performing action a in situation s. A fluent is a predicate or function whose last argument is a situation, and thus whose value can change from situation to situation. Actions need not be executable in all situations, and the predicate Poss(a, s) states that action a is executable in situation s. Actions have sensing results, and the function sr(a, s) denotes the sensing result of action a when executed in situation s [Scherl and Levesque, 2003].

Here, we restrict our attention to a situation calculus language L that includes only the function symbols do, sr, S0 as described above, the predicate symbol Poss, a finite number of functional 1 fluent symbols F, a finite number of action function symbols A whose arguments are of sort object, and a finite number of constant symbols C of sort object.

Within L, we can formulate action theories that describe how the world changes as the result of the available actions. We focus on a variant of the basic action theories [Reiter, 2001]. An action theory D has the following form: 2

1. Dap is a set of action precondition axioms, one per action symbol A, of the form Poss(A(⃗y), s) ≡ ΠA(⃗y, s).
2. Dss is a set of successor state axioms (SSAs), one for each fluent symbol f, of the form f(⃗x, do(a, s)) = v ≡ Φf(⃗x, a, v, s). SSAs characterize the conditions under which the fluent has a specific value at situation do(a, s) as a function of situation s.
3. Dsr is a set of sensing-result axioms (SRAs), one for each action symbol A, of the form sr(A(⃗y), s) = r ≡ ΘA(⃗y, r, s). SRAs relate sensing outcomes with fluents.
4. Duna is the set of unique-names axioms for actions: A(⃗x) ̸= A′ (⃗y), and A(⃗x) = A(⃗y) ⊃ ⃗x = ⃗y.
5. D0 is a set of axioms describing the initial situation S0.
6. Dfnd consists of the axioms for equality and a set of domain independent foundational axioms which formally define legal situations.

1 Relational fluents can be represented by functional fluents that are forced to take only values true/false. Non-fluent functions and predicates can be formalized as unchanging fluents [Reiter, 2001].

2 We will be omitting leading universal quantifiers.

1. E is a set of unique-names axioms for constants along with a domain closure axiom for sort object.

To describe actions along with their sensing results, we use terminology as in [De Giacomo et al., 2001]. A history h is a sequence (a1, r1) · . . . · (an, rn), where each ai is a ground action term and ri is a constant that represents the action's sensing outcome. We assume that non-sensing actions always return the fixed result c. We use end(h) as an abbreviation for the ground situation term that corresponds to h. This is defined as follows: end(h) is S0 for the empty history, and end(h · (a, r)) is do(a, end(h)). Similarly, S(h) is the set of atoms that describe the sensing results in h. S(h) is an abbreviation for {sr(ai, end(hi)) = ri | 1 ≤ i ≤ n}, where hi is the sub-history up to action ai, (a1, r1)·. . .·(ai-1, ri-1).

A situation-suppressed expression is a formula in the language without Poss and sr, and with all situation arguments suppressed. φ[σ] denotes the situation calculus formula obtained from φ by restoring the situation argument σ into all fluents in φ. We use a, b, c, d, e to range over C and f, g to range over F. A primitive fluent term is a ground term that mentions at most one fluent symbol, e.g. f(c, S0), and a primitive atom is one that mentions at most one primitive fluent term, e.g. f(c, S0) = d, f(c, S0) = x. A primitive formula (sentence) is a formula (sentence) that mentions only primitive atoms. Note that quantification is allowed in primitive formulas but not when the variable appears as an argument of a fluent. Finally, we use τ, u to denote a situationsuppressed primitive fluent term.

In this notation, the projection task [Reiter, 2001] is the following: given a history h and a situation-suppressed sentence φ, determine whether or not D∪S(h) |= φ[end(h)]. We propose to solve it for certain restricted action theories using a form of progression, which we define along the lines of [Lin and Reiter, 1997] and [Liu and Levesque, 2005]. Let I be a standard model iff I satisfies E.

Definition 1. Let I be a standard model of D0. I ′ is a successor model of I wrt a world-changing action A(⃗e) iff I ′ is a standard model and for any primitive fluent atom f(⃗c) = d[S0], I ′ |= f(⃗c) = d[S0] iff I |= Φf(⃗c,A(⃗e), d)[S0]. For a sensing action A(⃗e) with result b, I ′ is a successor model of I iff I ′ is a standard model, and I ′ |= f(⃗c) = d[S0] iff I |= f(⃗c) = d[S0] and I |= ΘA(⃗e, b)[S0].

Definition 2. D′0 is a progression of D0 wrt (A(⃗e), b) iff the standard models of D′0 are exactly the successor models of D0 wrt (A(⃗e), b).

One step of progression is a solution to one step of projection in the sense that if h = (a, r) and D∪S(h) is consistent, then D∪ S(h) |= φ[end(h)] iff D′0 |= φ[S0].

3 Possible values and bounded action theories

Although we are assuming that every fluent is functional, and thus has a single value, we do not assume that this value is known. For example, to say that the value of the fluent age in situation S0 might be 19, 20 or 21, D may contain the following disjunction: (age = 19 ∨ age = 20 ∨ age = 21)[S0]. Thus, we say that 19, 20 and 21 are the possible values that the fluent age can take. 3 As another example, suppose that we have the following sentence in D:

In this case, the fluents f and g each have two possible values. But because of the constraint between them, we should consider the pair 〈f, g〉 which has two (rather than four) possible values: 〈1, 0〉 and 〈0, 1〉. More generally, we have the following definition:

Definition 3. Let ⃗τ be a tuple of distinct situation-suppressed primitive fluent terms. A finite set of constant tuples V = {⃗ c1, . . . , ⃗ cn}, each of the same length as ⃗τ is the set of possible values for ⃗τ at history h iff V is the smallest set such that D ∪ S(h) |= (∨ni=1 ⃗τ = ⃗ ci)[end(h)]. Each element of V is a possible value of ⃗τ at h.

Note that V is the empty set only if D∪S(h) is inconsistent. When we say that a sentence is possibly true, we mean that it is entailed for some possible value of the fluents in the sentence, taking into account that some fluents may be grouped with others because of constraints.

Definition 4. Let h be a history and let φ be a situationsuppressed primitive sentence. Let T = {⃗ τ1, . . . , ⃗ τk} be a set of tuples of situation-suppressed primitive fluent terms such that every primitive fluent term in φ appears in exactly one ⃗τi. We say that φ is possibly true at history h wrt T iff E |= φ′ , where φ′ is φ with each ⃗τ ∈ T replaced by one of its possible values at h. (A tuple 〈τ1, . . . , τn〉 is replaced by 〈c1, . . . , cn〉 by replacing each term τi by the corresponding ci.)

We say that φ is known to be true at h wrt T iff ¬φ is not possibly true at h wrt T .

It is not hard to see that a sentence φ is known to be true at h iff for every possible value of the fluents at h, the substituted φ′ obtained is indeed entailed. But this is not the same thing as saying that φ[end(h)] itself is entailed by D∪ S(h). This depends on how we group the fluent terms into tuples.

Example 1. Consider a theory D containing the above sentence about f and g. Let h be the empty history and let φ be (f ̸= g). Then we have the following:

1. D∪ S(h) |= φ[end(h)];
2. φ is not known to be true at h wrt {f, g};
3. φ is known to be true at h wrt {〈f, g〉}.

What is going on here is that for T = {f, g} we look at the possible values of f and g independently, including cases where f = g. For T = {〈f, g〉} on the other hand, we only look at the two possible values for 〈f, g〉, and so rule out the cases where f = g.

This idea of fluent terms taking values independently is very much related to the weak disjunctive knowledge property defined in [Petrick and Levesque, 2002; Petrick, 2006] for an epistemic setting of the situation calculus. Our account here generalizes this idea by allowing tuples of fluent terms.

What we will be proposing in this paper, is a method of computing progression under incomplete knowledge that uses the possible values of fluent terms as above. To ensure that we get a T that correctly captures any constraints among the fluents, we will restrict the form of the basic action theory. The main idea behind what we call a bounded action theory is that D0 will explicitly list the initial possible values of the fluents according to some grouping T, and that the bodies of the successor state and sensing-result axioms will be suitable for specifying a new grouping T ′ such that what is known about the fluents after some action is performed is accurately captured by the new grouping T ′.

3 Note that this notion of possibility has an epistemic flavor and is distinct from the physical possibility of action execution, as characterized by P oss.

Definition 5. Let T = {⃗ τ1, . . . , ⃗ τk} be a set of tuples of situation-suppressed primitive fluent terms such that every primitive fluent term appears in exactly one ⃗τi. We say that D is local-effect and bounded by T iff the following all hold:

1. D0 = {α1[S0], . . . , αk[S0]}, where for each i, there is a set C of constant tuples such that αi is ∨⃗c∈C ⃗ τi = ⃗c.
2. Each successor state axiom in Dss has the form

where γf (⃗x, a, v) is a disjunction of formulas γ if (⃗x, a, v) of the form ∃⃗z(a = A(⃗y) ∧ψ(⃗y)), ⃗ y contains ⃗x ∪ {v}, ⃗z is the remaining variables of ⃗y, and ψ is a primitive formula that is called the context of γ if (⃗x, a, v).

1. Each sensing result axiom in Dsr has the form sr(A(⃗y), s) = r ≡ ΘA(⃗y, r)[s], where ΘA(⃗y, r) is a primitive formula.
2. Each precondition axiom in Dap has the form Poss(A(⃗y), s) ≡ ΠA(⃗y)[s], where ΠA(⃗y) is a primitive formula.
3. Each action symbol A is either a sensing action or a world-changing action and appears exclusively in exactly one SRA or in some SSAs, respectively.
4. If action symbol A appears in γf then it cannot appear in γg for any fluent g that appears in γf .

Local-effect and bounded action theories have the property that for any pair of ground action term A(⃗e) and sensing result b, both ΘA(⃗e, b) and ΠA(⃗e) are primitive sentences and γ if (⃗x, A(⃗e), v) is logically equivalent to (⃗x = ⃗c ∧ v = d ∧ φ), where ⃗c, d are contained in ⃗e and φ is a primitive sentence. These theories are restricted in that if an action A(⃗e) changes the value of a fluent term f(⃗c), then ⃗c is contained in the arguments of the action.

4 Progression using databases

Given an action theory D that is local-effect and bounded by T, we will use a database to represent the possible values for each τ in T, as a way to capture the models of D0. Then we will define a procedure PROG that transforms this database into one that represents a progression of D0.

We first review some basic notions of relational database theory. Let L be a first-order language with a finite number of predicate symbols and a finite number of constant symbols C. A database instance for the language L is a first-order structure I such that the domain of I is C, = is interpreted

φ := DBQ(ΘA(⃗e, b)) ⃗τ := ⃗τ1 · ⃗τ2 · · · · · ⃗τk, where R⃗τ1 , . . . , R⃗τk are the relation names in φ T := T -{⃗τ1, . . . , ⃗τk}+{⃗τ} I0 := I0 -{R⃗τ1 , . . . ,R⃗τk }+{R⃗τ}, where the extension of R⃗τ is φ(I0)

as identity, and each constant is interpreted as itself. Let ⃗x, ⃗y be tuples of variables. An ⃗x-relation over I is a finite set of mappings ζ from ⃗x into C, which we write as {ζ : [⃗x → C]}. Let φ be a formula with free variables ⃗x = 〈x1, . . . , xn〉. The answer to φ wrt I is the ⃗x-relation

Definition 6. Let L0 be the language that has the constants in C, and for each ⃗τ ∈ T the relation name R⃗τ with arity |⃗τ|. We define I0, the database that represents D0, as the database instance for language L0 such that the interpretation of each R⃗τ is the set of constant tuples C that appear in the corresponding α[S0] ∈ D0, in item 1 of Definition 5.

The following definition shows how to transform a primitive situation calculus formula φ into a query DBQ(φ) of L0. We will need to use a set of new variables, and we assume that there is a mapping ξ from primitive fluent terms to these variables such that each term is mapped to a distinct variable.

Definition 7. Let φ be a situation-suppressed primitive formula. Let φ′ be φ with each primitive fluent term replaced by the corresponding variable wrt the mapping ξ. Let T ′ ⊆ T be the smallest set such that ⃗τ ∈ T ′ if some element of ⃗τ appears in φ. We define DBQ(φ) as the formula

Now, on to progression. Here is how PROG[I0,A(⃗e), b] works when A is a sensing action: The fluents that are affected are those that appear in ΘA(⃗e, b). We use the concatenation of all the ⃗τi ∈ T that mention these fluent terms to construct a new relation. The tuples in this relation will be the answers to the query DBQ(ΘA(⃗e, b)). The progression for a world-changing action is more complex. For each fluent term f(⃗c) that is potentially given value d by action A(⃗e) according γf , we collect all the ⃗τi ∈ T that contain either f(⃗c) or a fluent term in the context, and we concatenate them together to make a new ⃗τ . We then assign R⃗τ to be the tuple of all possible values for these terms, using both the new value d for f(⃗c) when the context is true and the previous values when the context is false.

Definition 8. Let I0 be a database, A(⃗e) be a ground action term, and b be a sensing result. Then the procedure PROG[I0, A(⃗e), b] is defined as follows:

1. if A is a sensing action, then do as in Figure 1;
2. if A is a world-changing action, then use Figure 2.

Now we are ready to present our main result:

Theorem 1 (Progression). Let D be a local-effect action theory that is bounded by T and (A(⃗e), b) be an action-sensing

for each f ∈ F do for each γ if (⃗x, a, v) in γf (⃗x, a, v) that mentions A do ⃗c := the subset of ⃗e that corresponds to ⃗x d := the element of ⃗e that corresponds to v ⃗u := the element of T that mentions f(⃗c) φ+:= R⃗u(ξ(⃗u)) ∧ DBQ(γ if (⃗x, A(⃗e), v)) φ-:= same as φ+ but with context formula negated Q+ := φ+(I0) but with the column corresponding to ξ(f(⃗c)) replaced by the value d in all rows Q:= φ-(I0) ⃗τ := ⃗τ1 · ⃗τ2 · · · · · ⃗τk, where R⃗τ1 , . . . , R⃗τk are the relation names in φ+ T := T -{⃗τ1, . . . , ⃗τk}+{⃗τ} I0 := I0 -{R⃗τ1 , . . . ,R⃗τk }+{R⃗τ}, where the extension of R⃗τ is Q+ ∪Qend for end for

result pair such that D ∪ S((A(⃗e), b)) is consistent. Let I0 be the database that represents D0. Then PROG[I0, A(⃗e), b] represents a progression of D0 wrt (A(⃗e), b).

The proof of Theorem 1 follows from the following lemma and the property of bounded theories listed in item 6 of Definition 5 which implies that the processing of fluents in the main loop of Figure 2 can be done in any order.

Lemma 2. Let φ be a situation-suppressed primitive sentence. Then, φ is possibly true at the empty history wrt to T iff there exists a standard model of D0 that satisfies φ[S0] iff DBQ(φ)(I0) is non-empty.

We conclude this section with an example.

Example 2. Consider the following scenario where an agent lives in a fantasy world of some role playing game. The agent is trapped inside a dungeon and in order to get out she has to unlock the main door and climb out. Unfortunately, the main door can only be unlocked by casting a magical spell. In particular, the agent has to cast the spell while being in the same room with a magical orb that is hidden somewhere in the dungeon, otherwise the spell has no effect. Finally, even though the agent cannot find the magical orb, she knows that it is hidden somewhere in rooms R1 or R2 of the dungeon.

For simplicity we use three (functional) fluents to represent this scenario: hero, orb, door which hold the location of the agent, the location of the orb, and the state of the door respectively. We use two actions: go(y), the agent moves to room y; cast(y), the agent casts a spell that magically instructs the door to change to state y. Also, we use the constants Cl,Op to represent the state of the door (closed, open) and R1, R2 for the two rooms.

Let D be an action theory such that D0 consists of the sentences door = Cl[S0], (orb = R1 ∨ orb = R2)[S0], and hero=R1[S0]; Dap consists of precondition axioms such that Πgo and Πcast are always true; and Dss consists of the SSAs such that γhero(a, v)[s] is a = go(v), γorb(a, v)[s] is false, and γdoor(a, v)[s] is a = cast(v) ∧ ∃z(hero = z ∧ orb = z).

D is local-effect and bounded by T = {agent, orb, door}, but it is not context-complete. The following figure shows the database that represents D0 and the transformed database after applying PROG once for action cast(Op), and after applying PROG two more times for go(R2) and cast(Op).

Note that after the three steps of progression the fluent door has exactly one possible value, Op, as intended.

Finally, to justify concerns about why this approach is better than just calculating all the possible worlds, the reader should imagine there being a large number of fluents with unknown value (e.g. other doors, objects) for which the database remains unchanged. A more detailed discussion follows.

5 Complexity analysis

We first review some results about the complexity of database queries of a certain form. The guarded fragment GF is the smallest set of formulas such that any existentially quantified sub-formula φ is conjoined with a guard, i.e. an atom containing all the free variables of φ [Andr´eka et al., 1998]. In [Gottlob et al., 2003] GF was extended to the k-guarded fragment GFk where up to k atoms may jointly act as a guard. When I is a database of size n such that the domain and all relations are sorted, and φ ∈ GFk is a formula of size l, then φ(I) can be computed in time O(lnk ) (see [Liu and Levesque, 2003]).

The complexity of PROG(I0, A(⃗e), b) is dominated by the evaluation of database queries of the form DBQ(φ). By Definition 7, it follows that DBQ(φ) is a k-guarded formula, where k is the number of relation names that appear in DBQ(φ). For any theory D, we let the width of D be the maximum k and the depth of D be the maximum length over all of the formulas γ if (⃗x, a, v) and ΘA(⃗y, r) in D. By Definition 8, we get the following:

Theorem 3. Let D be a local-effect action theory that is bounded by T and (A(⃗e), b) be an action-sensing result pair. Let I0 be the database that represents D0. Then, the complexity of PROG[I0,A(⃗e), b] is O(lnk+1 ), where l is the depth and k is the width of D, and n is the size of I0.

The tractability of the approach relies on the assumption that the width of D is often a small constant K. (Note that the width of D is bounded by what we are calling the depth of D.) There is also one more issue: As we saw in Example 2, after a progression step is performed some of the relations in I0 may be joined together in the updated database and eventually this can lead to an exponential blow-up of the size of the database.

Nevertheless, we expect that in real-world domains there is a small upper-bound on the number of primitive fluent terms that are both unknown and mutually constrained at any history, and thus need to appear in the same relation in I0. Also assuming that there is a constant upper-bound for the number of possible values that a single fluent may have at any history then the size of the largest relation in I0 is always bounded by a large constant N.

With the current definition of PROG, the size of the relations in I0 may not be optimal because fluents that are known to be true may not be stored in a separate relation, such as hero in Example 2. This can be avoided by augmenting PROG to check, as a final step, whether some of the updated fluents have only one possible value and should be stored separately. Finally, following the proof of the complexity result about GFk in [Liu and Levesque, 2003], note that n is the size of the largest relation in I0. Hence, under the stated assumptions the complexity of PROG[I0,A(⃗e), b] is O(lN K+1 ), where l is the depth of D, and K, N as above.

6 RelatedWork

One of the main differences between our approach and most of the related work in the literature is that we work with functional fluents. Our intuition is that when it comes to restricted forms of incomplete knowledge, functional fluents with possible values are an attractive alternative. In a formalism with relational fluents (such as [Son and Baral, 2001; Liu and Levesque, 2005]) it is not clear how to handle information of the form (age = 19 ∨ age = 20 ∨ age = 21) without using a general method for unrestricted disjunctions, which will have computational problems of its own. Our way of handling the disjunctions by using a database of possible values is similar to ideas in [Antova et al., 2007] (where, however, actions and progression are not handled).

One serious limitation of our approach is that we are forced to represent all the primitive fluent terms in the language. Also, the theories we are dealing with are essentially propositional and we insist that an action does not affect both a fluent and its context. The approach of [Liu and Levesque, 2005] does not suffer from these limitations. Nevertheless, our progression mechanism is always logically correct, unlike the weak progression mechanism that is employed by Liu and Levesque which is logically complete only for theories that are context-complete. An example of the theories that we can handle better is illustrated at the end of Section 4.

One approach that is very similar in spirit to our own is that of the FLUX system for implementing fluent calculus theories [Thielscher, 2004]. FLUX can express incomplete knowledge in the form of finite domain arithmetic constraints that are handled by constraint handling rules [Fr¨uhwirth, 1998]. When incomplete knowledge is progressed in FLUX, new constraints that represent the progression are appended to the constraint store. When fluents remain unknown and are constantly progressed, the "chain" of stored constraints becomes larger which, apart from affecting the efficiency of reasoning, can lead to failure due to lack of memory resources. So while FLUX can be more efficient in computing the progression of a state after an action has been executed, appending constraints can be problematic for long-lived agents.

Another similar approach is that of [Funge, 1998], dealing with real-valued functional fluents. Unlike our approach though, Funge's does not provide a mechanism for joining fluents together whenever they are related with some constraint. Other related approaches for doing approximate progression of action theories include (approximate) logical filtering [Amir and Russell, 2003], and the 0-approximation semantics for an extension of the action language A [Son and Baral, 2001]. Finally, the idea of reasoning with possible values has been applied in an iterative planner [Levesque, 2005]

and in a variant of GOLOG [Sardina and Vassos, 2005].

7 Conclusion

In this paper, we have proposed a new progression mechanism for a restricted form of situation calculus basic action theories that feature incomplete knowledge and sensing. Our approach handles theories which are essentially the functional version of the local-effect action theories [Liu and Levesque, 2005], further restricted so that they are also bounded by a set of groupings for fluents. We use a large database in order to represent the models of a theory by dealing directly with the possible values that these groupings of fluents may have. Our progression mechanism updates the database according to how the possible values are affected by both worldchanging and sensing actions. The method we propose is logically complete and can be calculated efficiently using database techniques under certain reasonable assumptions.

Our current and future work focuses on some of the limitations of our approach. We are investigating alternative formalisms for representing D0 so that we avoid listing all primitive fluent terms in the language as well as all the possible values for each fluent. In particular, we consider the incorporation of intervals as a way to concisely represent large lists of possible values and the use of quantified axioms in D0. Furthermore, we believe that the local-effect requirement can be lifted with a small additional cost in the progression mechanism. Finally, we want to extend our approach so that it can handle the evaluation of unrestricted quantified formulas.