Tractable Reasoning with Incomplete First-Order Knowledge in Dynamic Systems with Context-Dependent Actions

1 Introduction

In the area of Knowledge Representation and Reasoning, there is a well-known tradeoff between the expressiveness of the representation language and the computational tractability of the associated reasoning task. At one extreme, we have databases for which queries can be efficiently evaluated. But databases are too limited for many AI applications because they require complete knowledge about the domains. Levesque [1998] proposes a generalization of a database called a proper KB, which allows a limited form of incomplete knowledge, equivalent to a (possibly infinite) consistent set of ground literals. Since the deduction problem for proper KBs is undecidable, Levesque proposes an evaluationbased reasoning procedure called V that is logically sound and, when the query is in a certain normal form called NF, also logically complete. Moreover, later Liu and Levesque [2003] show that despite the incomplete knowledge, database techniques can be used to implement V efficiently.

In this paper, we apply the procedure V to reasoning in dynamic systems where the state of the world changes as a result of the actions of agents. For such applications, a basic reasoning problem is the so-called projection problem: given an action theory that specifies the preconditions and effects of actions, and an initial KB, determine whether or not a formula holds after a sequence of actions is performed. Two settings where this problem arises naturally are for planning and for high-level program execution [Levesque et al., 1997]. A prerequisite to planning is the ability to determine if a goal is satisfied after a sequence of actions. To execute a high level robotic program such as "while there is a block on the table, pick up a block and put it away", one needs to determine after various sequences of actions whether there is still a block on the table.

1 By "tractable" we mean "solvable in polynomial time".

In practice, there are two ways to deal with projection: we can progress the initial KB wrt the action sequence and answer the query against the resulting KB; or we can regress the query wrt the action sequence and answer the resulting query against the initial KB. Progression has at least two advantages: First, it avoids a duplication of effort when multiple queries need to be answered wrt the same action sequence, and especially when that sequence is long. Second, in a robotics setting, a robot can use its "mental idle time" to compute a progression while it is busy performing physical actions. Projection via progression has three main computational requirements: the new KB must be efficiently computed, its size should be at most linear in the size of the initial KB (to allow for iterated progression), and it must be possible to answer the query efficiently from the new KB. Lin and Reiter [1997] give a formal study of progression. They show that progression is not always first-order definable, and identify a few important cases where progression is first-order definable and computationally tractable. However, the third requirement is not addressed in their paper.

In this paper, we propose a tractable, sound, and sometimes complete solution to the projection problem in the presence of incomplete first-order knowledge and context-dependent actions. We restrict our attention to actions with only "local" effects, and where incomplete knowledge is in the form of a proper KB. We define a version of progression where a proper KB remains proper afterward, and where applying V to the progressed KB and the query returns the same value as applying V to the initial KB and a regressed query. We prove that when the query is in NF and the initial KB has complete knowledge about the context of any context-dependent actions, our solution is logically complete. It is also logically complete when the query is in NF and there are sensing actions that provide dynamic information about the context of the relevant context-dependent actions.

2 Preliminaries

In this section, we review proper KBs, V, and NF. Also, we briefly review the situation calculus, and formally define local-effect action theories and regression for them.

2.1 Proper KBs, V, and the normal formNF

We use a standard first-order logical language L with equality, a countably infinite set of constants C = {c1, c2, . . .}, and no other function symbols. We restrict our attention to standard interpretations, where equality is identity, and there is a bijection between the set of constants and the domain of discourse. This restriction can be captured by a set of axioms E, consisting of the axioms of equality and the set of formulas {ci ̸= cj | i ̸= j}. Since we treat equality separately, when we say "predicate", "atom" or "literal", we exclude equality.

We use ρ to range over atoms whose arguments are distinct variables. We use e to range over ewffs, that is, quantifier-free formulas with only equalities (i.e. no predicates). We use ∀φ to denote the universal closure of φ. We write φxc to denote φ with all free occurrences of x replaced by constant c. We write Σ |=E φ to denote E ∪ Σ |= φ.

Definition 1 A KB Σ is proper if E ∪ Σ is consistent and Σ is a finite set of formulas of the form ∀(e ⊃ ρ) or ∀(e ⊃ ¬ρ).

It is not hard to see that the problem of determining whether a sentence is logically entailed by a proper KB is undecidable, since when the KB is empty, this reduces to classical validity. Levesque [1998] proposes an evaluation-based reasoning procedure called V instead. Given a proper KB and a query, V returns one of three values 0 (known false), 1 (known true), or 12 (unknown) as follows:

1. V [Σ, c = c′ ] = 1 if c is identical to c′ , and 0 otherwise;
2. V [Σ, ¬φ] = 1-V [Σ, φ];
3. V [Σ, φ ∨ψ] =max{V [Σ, φ], V [Σ, ψ]};
4. V [Σ, ∃xφ] = maxc∈H+ V [Σ, φxc ], where H + is the union of the constants in Σ or φ, and an extra constant.

This V procedure is logically sound and, when the query is in a certain normal form called NF, also logically complete:

Theorem 1 ([Levesque, 1998]) Let Σ be proper. Then

1. for every φ ∈ L, if V [Σ, φ] = 1 then Σ |=E φ; and if V [Σ, φ] = 0 then Σ |=E ¬φ.
2. for every φ ∈ NF, V [Σ, φ] = 1 iff Σ |=E φ; and V [Σ, φ] = 0 iff Σ |=E ¬φ.

For the interested readers, the following is the definition of NF from [Levesque, 1998]:

Definition 2 A set Γ of sentences is logically separable iff for every consistent set of ground literals L, if L ∪ Γ has no standard model, then L∪{φ} is inconsistent for some φ ∈ Γ.

Definition 3 The normal formNF is the least set such that

1. if φ is a ground atom or ewff, then φ ∈ NF;
2. if φ ∈ NF, then ¬φ ∈ NF;
3. if φ1, . . . , φn ∈ NF, and {φ1, . . . , φn} is logically separable, then ∧φi ∈ NF;
4. if Γ ⊆ NF, Γ is logically separable, and for some φ, Γ = {φxc | c ∈ C}, then ∀xφ ∈ NF.

The intuition behind NF is that different parts of a formula must be logically independent. A simple example of a formula not in NF is (p ∨¬p), where p is atomic. In the propositional case, a CNF formula is in NF if its clauses are nontautologous and closed under resolution.

Liu and Levesque [2003] show that V can be implemented efficiently using database techniques (projections, joins, etc). Here we present a cleaner variant of this result.

Let Lk denote the set of formulas from L that use at most k different variables. Let R = {⃗c 1, . . . , ⃗c m} be a finite set of n-tuples. We use ⃗x ∈ R to denote ⃗x = ⃗c 1 ∨ . . . ∨ ⃗x = ⃗c m.

Definition 4 Let L be P or ¬P for some predicate P. The ewff defining L in a proper Σ, denoted by ξL, is the disjunction of all e such that ∀(e(⃗x) ⊃ L(⃗x)) ∈ Σ. We can write ξL in the form of ⃗x ∈ IL ∨ eL ∧ ⃗x ̸∈ OL so that IL and OL are finite relations with as many tuples as possible, and eL is an ewff. The e-size of Σ is the maximum size of an eL in Σ.

Then a corollary to Theorem 4.8 in [Liu and Levesque, 2003]: Corollary 2 Let Σ be proper, and let φ ∈ Lk . Then V [Σ, φ] can be computed in time O(lmnk ), where l is the size of φ, m is the e-size of Σ, and n is the size of Σ.

Although the time complexity scales exponentially with k, this is typical even of queries over ordinary databases, and so is perhaps as good as can be expected.

2.2 Situation calculus

Our account of action and change is formulated in the language of the situation calculus [McCarthy and Hayes, 1969; Reiter, 2001]. We will not go over the language here except to note the following components: there are three disjoint sorts for actions, situations, and objects; there is a special constant S0 denoting the initial situation, namely the one in which no actions have yet occurred; there is a distinguished binary function do(a, s) denoting the successor situation to s resulting from performing action a; relations whose truth values vary from situation to situation, are called (relational) fluents, and are denoted by predicate symbols taking a situation term as their last argument; and there is a special predicate Poss(a, s) stating that action a is executable in situation s.

We relate the language of the situation calculus to L as follows: There is a set of constants of sort object which are constants of L. The situation-independent predicates and relational fluents are predicates from L. That is, if P(⃗x) is a situation-independent predicate, and F(⃗x, s) is a relational fluent, then P(⃗x) and F(⃗x) are predicates from L.

We extend the language L to L+ by allowing equalities involving action functions. Let φ ∈ L+, and let τ be a situation term. We use φ[τ] to denote the situation calculus formula obtained from φ by taking τ as the situation arguments of all fluents mentioned by φ. We use α to range over ground actions, and we use δ to range over sequences of ground actions.

Let δ = 〈α1, . . . , αn〉. We use do(δ, S0) to denote the end situation of δ, that is, do(αn, do(αn-1, . . . do(α1, S0) . . .)).

A particular domain of application will be specified by a basic action theory of the following form: 2

1. Dap is a set of action precondition axioms, one for each action function A, with form Poss(A(⃗x), s) ≡ ΠA(⃗x)[s], 3 where ΠA(⃗x) ∈ L.
2. Dss is a set of successor state axioms (SSAs), one for each fluent, of the form F(⃗x, do(a, s)) ≡ ΦF (⃗x, a)[s], where ΦF (⃗x, a) ∈ L+. Usually, ΦF (⃗x, a) has the form

SSAs take the place of the so-called effect axioms, and provide a solution to the frame problem.

1. Duna is the set of unique names axioms for actions:

where A and A′ are distinct action functions.

1. DS0 is of the form {φ[S0] | φ ∈ Σ0}, where Σ0 ⊆ L. Σ0 is called the initial KB.

In this setting, the projection task can be defined as follows: determine if D |=E φ[do(δ, S0)], where φ ∈ L, and δ is a sequence of ground actions.

As a running example, we will use a simple blocks world. 4 We use a single action, move(x, y, z), moving a block x from block y to block z (treating the table as just another block). We use three fluents: clear(x, s), block x has no blocks on top of it; on(x, y, s), block x is on block y; eh(x, s), the height of block x is even. We have the following action precondition axiom and successor state axioms:

P oss(move(x, y, z), s) ≡ clear(x) ∧ on(x, y) ∧ clear(z).

2.3 Local effect action theories and regression

Actions in many dynamic domains have only local effects in the sense that if an action A(⃗c ) changes the truth value of an atom F(⃗ d ), then ⃗ d is contained in ⃗c . This contrasts with actions having universal effects such as exploding a bomb, which kills all those near it. We can define this as follows:

Definition 5 A successor state axiom is local-effect if both γ+ F (⃗x, a) and γF (⃗x, a) are disjunctions of formulas of the form ∃⃗z [a = A(⃗y) ∧ φ(⃗y)], where A is an action function, ⃗y contains ⃗x, ⃗z is the remaining variables of ⃗y, and φ (called a context formula) is a quantifier-free formula from L. An action theory is local-effect if each SSA is local-effect.

2 We use slightly different notation from that in [Reiter, 2001].

3 We omit the leading universal quantifiers.

4 To justify the concerns for the tractability of reasoning, the reader should imagine there being a very large number of blocks.

Our blocks world example above is clearly local-effect.

The notion of a successor state axiom being local-effect is a generalization of that of being strictly context-free defined by Lin and Reiter [1997]. An SSA is strictly contextfree if γ+ F (⃗x, a) and γF (⃗x, a) are disjunctions of formulas of the form ∃⃗z [a = A(⃗y)], where A, ⃗y, and ⃗z are as above. For instance, the SSA for fluent on is strictly context-free, while that for fluent eh is not.

By using the unique names axioms, the instantiation of a local-effect SSA on a ground action can be significantly simplified . Suppose the SSA for F is local-effect. Let α = A(⃗c) be a ground action, and let ∗ be + or -. Then γ ∗F (⃗x, α) is equivalent to a formula of the following form:

where ⃗ di is a vector of constants contained in ⃗c, and ψi is a sentence. We will use γ ∗F (α)(⃗x) to denote the above formula, and we will write (⃗ d, ψ) ∈ γ ∗F (α) to mean that ⃗x = ⃗ d ∧ ψ is one of the disjuncts. Also, we will use ΦF (α)(⃗x) to denote γ+ F (α)(⃗x) ∨ (F (⃗x) ∧ ¬γF (α)(⃗x)). In the case of our blocks world, instances of the SSAs can be simplified as follows:

An important computational mechanism for reasoning about actions is regression [Reiter, 2001]. Here we define a one-step regression operator for local-effect action theories.

Definition 6 Let φ ∈ L. We use Rα(φ) to denote the formula obtained from φ by replacing each fluent atom F(⃗t ) with ΦF (α)(⃗t ). We call Rα(φ) the regression of φ wrt α.

Note that Rα(φ) remains in L. Let δ = 〈α1, . . . , αn〉. We use Rδ to denote Rα1 ◦ · · · ◦ Rαn . We now state a simple form of the regression theorem [Reiter, 2001]. Recall that Σ0 is the initial KB of D.

Theorem 3 (The Regression Theorem)

This theorem shows that regression is a sound and complete solution to the projection problem. In this paper, we prove all our results about progression by using regression as a bridge.

3 Progression of Proper KBs

In this section, we define a variant of classical progression, and show how to compute it for local-effect action theories.

First consider classical progression. Suppose we have a KB Σ. Let M be a possible state of Σ, that is, a model of Σ. Let α be a ground action. Then the successor state of M wrt α is the model M ′ such that for any ground fluent atom F (⃗c ), M ′ |= F(⃗c ) iff M |= ΦF(α)(⃗c ). A KB Σ′ is a progression of Σ wrt α if the models of Σ′ are exactly the successor states of models of Σ wrt α. A basic property of progression is: Suppose that Σ′ is a progression of Σ wrt α. Then for every φ ∈ L, Σ′ |=E φ iff Σ |=E Rα(φ). It is in this sense that we say classical progression preserves classical entailment.

It would be nice if the classical progression of a proper KB were proper, so that we could use it and V to solve the projection problem. However, this is unfortunately not the case even for very simple action theories. Consider the following example from [Petrick and Levesque, 2002]:

Then any progression of the empty KB (which is proper) wrt action A results in disjunctive information, (F ∨ ¬G), and hence is no longer proper. So what we will propose is a variant of classical progression where the progression of a proper KB does remain proper and the progression preserves V instead of preserving classical entailment.

Definition 7 Let Σ and Σ′ be proper. We say that Σ′ is a (weak) progression of Σ wrt a ground action α if for every φ ∈ L, V [Σ′ , φ] = V [Σ, Rα(φ)].

We now show that for local-effect action theories, it is easy to compute a weak progression of a proper KB.

Definition 8 Let D be local-effect and Σ be proper. We define Pα(Σ) as the set of the following sentences:

where F ranges over fluents, ξF (resp. ξ¬F ) is the ewff defining F (resp. ¬F) in Σ (c.f. Definition 4), and

Then we get the following:

Theorem 4 Let D be local-effect and Σ be proper. Then Pα(Σ) is a weak progression of Σ wrt α.

Let δ = 〈α1, . . . , αn〉. We use Pδ to denote Pαn ◦ · · · ◦ Pα1 . By a simple induction, we have that for every φ ∈ L, V [Pδ(Σ), φ] = V [Σ, Rδ(φ)].

The intuition behind AF and D¬F is simple. For ⃗ d ∈ AF , F (⃗ d ) will become true in every possible successor state, so we add F(⃗ d ) to Σ. For ⃗ d ∈ D¬F , F(⃗ d ) may become true in some possible successor state, so we delete ¬F ( ⃗ d ) from Σ. Now consider our blocks world example. Let Σ = {on(c1, c2), clear(c1), clear(c3), eh(c1)}. After action move(c1, c2, c3) is performed, we add clear(c2), ¬clear(c3), on(c1, c3), and ¬on(c1, c2) to Σ, and delete clear(c3), ¬clear(c2), on(c1, c2), ¬on(c1, c3), eh(c1), and ¬eh(c1) from Σ. We delete eh(c1) because if eh(c3) holds in the current state, eh(c1) will become false in the successor state; similarly, we delete ¬eh(c1).

We now define a reasoning procedure PV to solve the projection task using weak progression and V as follows:

Definition 9 Let D be a local-effect action theory with a proper Σ0. We define PV [δ, φ] as V [Pδ(Σ0), φ].

Now suppose that PV [δ, φ] = 1. Then V [Σ0,Rδ(φ)] = V [Pδ(Σ0), φ] = 1. By soundness of V , Σ0 |=E Rδ(φ). By the Regression Theorem, D |=E φ[do(δ, S0)]. Similarly, if PV [δ, φ] = 0, then D |=E ¬φ[do(δ, S0)]. Thus PV is logically sound for projection. It is easy to see that Pα(Σ) can be computed in O(n) time, where n is the size of Σ. By Corollary 2, we have the following tractability result:

Theorem 5 Let D be a local-effect action theory with a proper Σ0, and let φ ∈ Lk . Then PV [δ, φ] can be computed in time O(pn + lmnk ), where p is the length of δ, l the size of φ, m the e-size of Σ0, and n the size of Σ0.

Thus PV provides an efficient and logically sound solution to the projection problem despite the incomplete knowledge. In the next two sections, we will explore under what conditions, PV is also logically complete.

4 ACompleteness Result

Since PV uses V , it is not surprising that we need a query to be in normal form for logical completeness. In this section, we will show that the only other thing we need is for the initial KB to have complete knowledge of the context of any context-dependent actions.

More precisely, we say that a KB Σ is complete wrt a set G of ground atoms if for all l ∈ G, either Σ |=E l or Σ |=E ¬l. A KB Σ is complete wrt a predicate P if it is complete wrt all ground atoms of P . Now let Σ be proper, and φ a quantifierfree sentence such that Σ is complete wrt all atoms of φ. Then it is easy to see that V [Σ, φ] is either 0 or 1.

Definition 10 A KB Σ is context-complete (wrt D) if it is complete wrt every predicate appearing in every γ+ F and γF .

So Σ is context-complete if it has complete knowledge about the predicates in the context of any context-dependent actions. For example, in our blocks world, a Σ is contextcomplete if it is complete wrt eh; it may be incomplete wrt clear and on. So context-completeness still allows incomplete knowledge.

There are two useful special cases where we get contextcompleteness. An SSA is equality-only if no predicate appears in γ+ F or γF . Obviously, any Σ is context-complete wrt equality-only SSAs. Indeed, many SSAs we come across are equality-only. An SSA is context-free if no fluent appears in γ+ F or γF . It is reasonable to assume that an agent has complete knowledge about situation-independent predicates. Under such an assumption, any Σ is context-complete wrt context-free SSAs.

The logical completeness of PV is obtained by showing that progression preserves context-completeness and that under context-completeness, our progression coincides with classical progression.

Theorem 6 Let Σ be context-complete. Then

1. Pα(Σ) is context-complete too;
2. Pα(Σ) is a classical progression of Σ.

Proof: (2) We prove that for every model M ′ , M ′ |= Pα(Σ) iff there is a model M s.t. M |= Σ and M ′ is the successor state of M wrt α. For the only-if direction, we construct M as follows: for every fluent atom F(⃗c ), if V [Σ, F(⃗c)] = 1, then M |= F(⃗c ); if V [Σ, F(⃗c)] = 0, then M |= ¬F(⃗c ); otherwise, M |= F(⃗c ) iff M ′ |= F(⃗c ). The proof uses the fact that V [Σ, γ ∗F (α)(⃗c )] ∈ {0, 1}, where ∗ is + or -.

So under context-completeness, our progression preserves classical entailment. Now let Σ0 be context-complete. By a simple induction, we have: for every φ ∈ L, Pδ(Σ0) |=E φ iff Σ0 |=E Rδ(φ). Now let φ ∈ NF. By completeness of V for NF, V [Pδ(Σ0), φ] =1 iff Pδ(Σ0) |=E φ iff Σ0 |=E Rδ(φ) iff D |=E φ[do(δ, S0)]. Thus when the initial KB is contextcomplete and the query is in normal form, PV is logically complete for projection.

5 Incorporating Sensing

In many applications, it is asking too much to require complete knowledge in the initial KB about the context of the context-dependent actions. In this section, we follow de Giacomo and Levesque [1999] and relax this restriction in two ways: first, we only need context-completeness relative to the sequence of actions and the query in question; second, we can achieve this local context-completeness dynamically by resorting to sensing actions, that is, actions that get knowledge from outside the system. In other words, we show that when a history of actions and sensing results is "just-in-time" for a normal form query, PV is once again logically complete.

We first extend our account of action and change to incorporate sensing. Assume that in addition to ordinary actions that change the world, we also have binary sensing actions that do not change the world but tell the agent whether some condition φ holds in the current situation. We use the predicate SF(a, s) to characterize what the sensing action tells the agent about the world. Now our basic action theory has an extra component Dsf , which is a set of sensed fluent axioms (SFAs), one for each action, of the form SF(A(⃗x), s) ≡ φA(⃗x)[s], where φA ∈ L. We say that Dsf is atomic if each φA is an atom.

For instance, we may add three sensing actions to the blocks world example: senseclear(x), senseon(x, y), and senseeh(x). The axiom SF(senseeh(x), s) ≡ eh(x, s) says that the action senseeh(x) tells the agent if eh(x, s) holds.

To describe a sequence of actions and sensing results, we use the notion of a history, that is, a sequence of pairs (α, µ) where α is a ground action and µ ∈ {0, 1} is the sensing result: when α is an ordinary action, we simply let µ = 1. We use end(σ) to denote the end situation of history σ, and Sensed(σ) to denote the situation calculus formula stating all sensing results of σ. Formally,

• end(ε) = S0, where ε is the empty history; end(σ · (α, µ)) = do(α, end(σ)).
• Sensed(ε) = True; Sensed(σ · (α, 1)) = Sensed(σ) ∧ SF (α, end(σ)); Sensed(σ · (α, 0)) = Sensed(σ) ∧ ¬SF (α, end(σ)).

Naturally, we are only interested in consistent histories, that is, histories with reasonable sensing results. Formally,

Definition 11 A history σ is consistent if

E ∪ D ∪ {Sensed(σ)} is a consistent theory.

Now the projection problem including sensing is formulated as deciding if D ∪ {Sensed(σ)} |=E φ[end(σ)], where φ ∈ L, and σ is a consistent history.

In the rest of this section, we assume that Dsf is atomic. To prepare for the definition of just-in-time-history, we first extend our regression and progression operators to incorporate sensing. The ideas are quite simple. For example, if we regress the formula clear(c1) ∧ eh(c1) wrt (senseeh(c1), 1), we should obtain clear(c1). If we progress a proper KB Σ wrt (senseeh(c1), 1), we should obtain Σ ∪ {eh(c1)}.

Let α = A(⃗c ) be a ground action, and let µ ∈ {0, 1}. We define R(α,µ)(φ) as follows: If α is an ordinary action, then R(α,µ)(φ) = Rα(φ). Otherwise, let the SFA be SF(A(⃗x), s) ≡ F(⃗x, s). Then R(α,µ)(φ) is the formula obtained from φ by replacing each atom F (⃗t ) with ⃗t = ⃗c ∨F (⃗t ) when µ = 1 and with F(⃗t ) ∧ ⃗t ̸= ⃗c when µ = 0. We have the following extended regression theorem:

Now we turn to progression with sensing. Let Σ be proper. Let α = A(⃗c ) be a ground action, and let µ ∈ {0, 1}. We define P(α,µ)(Σ) as follows: If α is an ordinary action, then P(α,µ)(Σ) = Pα(Σ). Otherwise, let the SFA be SF(A(⃗x), s) ≡ F(⃗x, s). Then P(α,1)(Σ) = Σ ∪ {F(⃗c )}, and P(α,0)(Σ) = Σ ∪ {¬F(⃗c )}. We have the following extended progression theorem:

Theorem 8 Let σ be a consistent history. Then

1. E ∪Pσ(Σ0) is consistent. Hence Pσ(Σ0) is proper.
2. For every φ ∈ L, V [Pσ(Σ0), φ] = V [Σ0, Rσ(φ)].

Another concept we need is dependency set.

Definition 12 The dependency set of a formula φ wrt an ordinary action α, denoted by DSα(φ), is the set of ground atoms that appear in γ+ F (α) or γF (α) for some fluent F in φ. For example, let α = move(c1, c2, c3). Then DSα(clear(x)) is the empty set, and DSα(eh(x)) = {eh(c3)}.

Definition 13 Let σ be a consistent history, and φ ∈ L. We say that σ is a just-in-time-history (JIT-history) for φ if for every division σ1 · (α, µ) · σ2 of σ such that α is an ordinary action, Pσ1 (Σ0) is complete wrt DSα(Rσ2 (φ)).

Intuitively, σ is a JIT-history for φ if whenever performing an ordinary action α, the agent has complete knowledge about the context of α wrt fluents related to φ. This complete knowledge may come from the sensing actions preceding α. For example, let Σ0 = {clear(c1), on(c1, c2), clear(c3)}. Then the history (senseeh(c3), 1) · (move(c1, c2, c3), 1) is a JIT history for the formula ∃x[clear(x) ∧ eh(x)]. Note that here the agent has incomplete knowledge about both fluents clear and eh. Thus a JIT history does not require complete knowledge about the component fluents of the query.

By a proof essentially the same as the one in the previous section, we get the following result:

Theorem 9 Let σ be a JIT-history for φ.

Then Pσ(Σ0) |=E φ iff Σ0 |=E Rσ(φ).

Now let σ be a JIT-history for φ ∈ NF. Then we have V [Pσ(Σ0), φ] = 1 iff Pσ(Σ0) |=E φ iff Σ0 |=E Rσ(φ) iff D ∪ {Sensed(σ)} |=E φ[end(σ)]. Thus when a history is just-in-time for a normal form query, PV is again logically complete for projection.

6 RelatedWork

As mentioned in the introduction, Lin and Reiter [1997] give a systematic study of classical progression. As a part of their study, they view STRIPS as a mechanism for computing progression and thus provide a logical semantics for STRIPS. In this respect, they consider strictly context-free SSAs and initial KBs in the form of relational databases or sets of ground literals. These are special cases of local-effect SSAs and proper KBs, and our weak progression coincides with classical progression in these cases. Son and Baral [2001] propose the so-called 0-approximation semantics for an extension of action language A. They define an a-state (approximate state) as a consistent set of fluent literals, and define a transition function which maps an a-state and an action into the next a-state. So 0-approximation is essentially a kind of approximate progression. However, their work is restricted to the propositional case, and our progression coincides with theirs therein. Amir and Russell [2003] present efficient algorithms for (approximate) logical filtering, where filtering means updating an agent's belief state in response to actions and observations. So logical filtering is essentially progression. But again, their work is restricted to the propositional case. De Giacomo and Mancini [2004] study how to exploit relational database technology to implement progression, but only when the initial KB has complete knowledge. We get to use database techniques in the incomplete case via the results in [Liu and Levesque, 2003].

The idea of progression is widely used in planning under incomplete knowledge. Most systems use propositional representations, for example, BDDs [Cimatti and Roveri, 2000], and clauses [Brafman and Hoffmann, 2004]. Being propositional makes it possible for them to consider arbitrary incomplete knowledge and perform classical progression. Although techniques are employed so that the systems can achieve reasonable performance in practice, there is no theoretical guarantee of the tractability of their solutions to projection. The PKS system of Petrick and Bacchus [2002] uses a first-order representation. The form of incomplete knowledge they consider is mainly a set of ground literals but with some other features. The general idea behind their progression is similar to ours, but without a semantical characterization of what it preserves. Moreover, they do not address the issue of the restrictions they need to get completeness.

The idea of JIT histories in this paper comes from [De Giacomo and Levesque, 1999]. They use JIT histories to obtain complete knowledge about the component fluents of the query. However, we use JIT histories only to obtain complete knowledge about the context of actions to be performed.

7 Conclusions

In this paper, we have proposed a tractable, sound, and sometimes complete solution to the projection problem in the presence of context-dependent actions and incomplete first-order knowledge in the form of a proper KB. Our solution is via a version of progression that preserves properness and V .

For simplicity of presentation, in this paper we require actions to have local effects only, and we make the extra requirement that context formulas (c.f. Definition 5) be quantifierfree. However, the soundness and completeness results in this paper will still hold if we relax these two requirements. The tractability result will also hold if context formulas use a bounded number of variables. As for local effects, the tractability result only needs them to ensure that the progressed KB is not much larger than the original KB. We believe that there are other ways of doing this that would include a substantial class of actions with universal effects.

For the future, we would like to conduct experimental evaluation of our solution to projection, and apply it to first-order planning systems. Also, we would like to extend our work here to deal with functional fluents and disjunctive incomplete knowledge.