On First-Order Definability and Computability of Progression for Local-Effect Actions and Beyond

1 Introduction

A fundamental problem in reasoning about action is projection, which is concerned with determining whether or not a formula holds after a number of actions have occurred, given a description of the preconditions and effects of the actions and what the world is like initially. Projection plays an important role in planning and in action languages such as Golog [Levesque et al., 1997] or A [Gelfond and Lifschitz, 1993].

Two powerful methods to solve the projection problem are regression and progression. Roughly, regression reduces a query about the future to a query about the initial knowledge base (KB). Progression, on the other hand, changes the initial KB according to the effects of each action and then checks whether the formula holds in the resulting KB. One advantage of progression compared to regression is that after a KB has been progressed, many queries about the resulting state can be processed without any extra overhead. Moreover, when the action sequence becomes very long, as in the case of a robot operating for an extended period of time, regression simply becomes unmanageable. However, projection via progression has three main computational requirements which are

Gerhard Lakemeyer

Dept. of Computer Science RWTH Aachen 52056 Aachen, Germany gerhard@cs.rwth-aachen.de

not easy to satisfy: 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.

As Lin and Reiter [1997] showed in the framework of Reiter's version of the situation calculus [Reiter, 2001], progression is second order in general. And even if it is firstorder (FO) definable, the size of the progressed KB may be unmanageable and even infinite. Recently, Vassos and Levesque [2008] also showed that the second-order nature of progression is in general inescapable, as a restriction to FO theories (even infinite ones) is strictly weaker in the sense that inferences about the future may be lost compared to the second-order version.

Nevertheless, for restricted action theories, progression can be FO definable and very effective. The classical example is STRIPS, where the initial KB is a set of literals and progression can be described via the usual add and delete lists. Since STRIPS is quite limited in expressiveness, it seems worthwhile to investigate more powerful action descriptions which still lend themselves to FO definable progression. Lin and Reiter [1997] already identified two such cases, and recently Vassos et al. [2008] were able to show that for so-called local-effect actions, which only change the truth values of fluent atoms with arguments mentioned by the actions, progression is always FO definable. However, they showed the computability of the FO representation only for a special case.

In this paper, we substantially improve and extend the results of Vassos et al.. By appealing to the notion of forgetting [Lin and Reiter, 1994], we show that progression for arbitrary local-effect actions is always FO definable and computable. We extend this result to certain actions with nonlocal effects like the briefcase domain, where moving a briefcase implicitly moves all the objects contained in it. For the special case of so-called proper+ KBs [Lakemeyer and Levesque, 2002] and a restricted class of local-effect actions we show that progression is not only first-order definable but also efficiently computable.

The rest of the paper is organized as follows. In the next section we introduce background material, including the notion of forgetting, Reiter's basic action theories, and progression. In Section 3 we present our result concerning localeffect actions. Section 4 deals with non-local effects and Section 5 with proper+ KBs. Then we conclude.

2 Preliminaries

We start with a first-order language L with equality. The set of formulas of L is the least set which contains the atomic formulas, and if φ and ψ are in the set and x is a variable, then ¬φ, (φ∧ψ) and ∀xφ are in the set. The connectives ∨, ⊃, ≡, and ∃ are understood as the usual abbreviations. To improve readability, sometimes we put parentheses around quantifiers. We use the "dot" notation to indicate that the quantifier preceding the dot has maximum scope, e.g., ∀x.P(x) ⊃ Q(x) stands for ∀x[P(x) ⊃ Q(x)]. We often omit leading universal quantifiers in writing sentences. We use φ ⇔ ψ to mean that φ and ψ are logically equivalent. Let φ be a formula, and let μ and μ′ be two expressions. We denote by φ(μ/μ′ ) the result of replacing every occurrence of μ in φ with μ′ .

2.1 Forgetting

Lin and Reiter [1994] defined the concept of forgetting a ground atom or predicate in a theory. Intuitively, the resulting theory should be weaker than the original one, but entail the same set of sentences that are "irrelevant" to the ground atom or predicate.

Definition 2.1 Let μ be either a ground atom P(⃗t) or a predicate symbol P . Let M1 and M2 be two structures. We write M1 ∼μ M2 if M1 and M2 agree on everything except possibly on the interpretation of μ.

Definition 2.2 Let T be a theory, and μ a ground atom or predicate. A theory T ′ is a result of forgetting μ in T , denoted by forget(T, μ) ⇔ T ′ , if for any structure M, M |= T ′ iff there is a model M ′ of T such that M ∼μ M ′ .

Clearly, if both T ′ and T ′′ are results of forgetting μ in T, then they are logically equivalent. Similarly, we can define the concept of forgetting a set of atoms or predicates. In this paper, we are only concerned with finite theories. So henceforth we only deal with forgetting for sentences.

Lin and Reiter [1994] showed that for any sentence φ and atom p, forgetting p in φ is FO definable and can be obtained from φ and p by simple syntactic manipulations. Here we reformulate their result in the context of forgetting a finite number of atoms. We first introduce some notation.

Let Γ be a finite set of ground atoms. We call a truth assignment θ of atoms from Γ a Γ-model. Clearly, a Γ-model θ can be represented by a conjunction of literals. We use M(Γ) to denote the set of all Γ-models. Let φ be a formula, and θ a Γ-model. We use φ[θ] to denote the result of replacing every occurrence of P(⃗t) in φ by the following formula:

where for j = 1, . . . ,m, the truth value of P(⃗tj) is specified by θ, and vj is the truth value.

Proposition 2.3 Let φ be a formula, M ∼Γ M ′ , θ ∈ M(Γ), and M |= θ. Then for any variable assignment σ, M, σ |= φ iff M ′ , σ |= φ[θ].

Proof: Let M be a structure. We show that M |= ∨θ∈M(Γ) φ[θ] iff there is a model M ′ of φ s.t. M ∼Γ M ′ . Suppose the latter. Let θ ∈ M(Γ) s.t. M ′ |= θ. By Proposition 2.3, M |= φ[θ]. Now suppose M |= φ[θ], where θ ∈ M(Γ). Let M ′ be the structure s.t. M ∼Γ M ′ and M ′ |= θ. By Proposition 2.3, M ′ |= φ.

Corollary 2.5

Example 2.1 Let φ = ∀x.clear(x),

and Γ = {clear(A), clear(B)}. Then

φ[clear(A) ∧ clear(B)]=∀x.x=A ∧ true∨x=B ∧ true

∨ x ̸= A ∧ x ̸= B ∧ clear(x), which is equivalent to

∀x.x = A ∨ x = B ∨ x ̸= A ∧ x ̸= B ∧ clear(x). Similarly,

φ[clear(A) ∧ ¬clear(B)] ⇔

∀x.x = A ∨ x ̸= A ∧ x ̸= B ∧ clear(x),

φ[¬clear(A) ∧ clear(B)] ⇔

∀x.x = B ∨ x ̸= A ∧ x ̸= B ∧ clear(x), and

φ[¬clear(A) ∧ ¬clear(B)] ⇔

∀x.x ̸= A ∧ x ̸= B ∧ clear(x).

Thus forget(φ, Γ) ⇔

We now assume L2 , the second-order extension of L.

Theorem 2.6 forget(φ, P) ⇔ ∃R.φ(P/R), where R is a second-order predicate variable.

Example 2.2 Let φ1 = ∀x.clear(x) ∨ ∃y.on(y, x). Then forget(φ1, clear) ⇔ ∃R∀x.R(x) ∨ ∃y.on(y, x), which is equivalent to true. Let φ2 = ∃x.clear(x) ∧ ∃y.on(x, y). Then forget(φ2, clear) ⇔ ∃R∃x.R(x) ∧ ∃y.on(x, y), which is equivalent to ∃x∃y.on(x, y).

In general, forgetting a predicate is not FO definable. Naturally, by Theorem 2.6, second-order quantifier elimination techniques can be used for obtaining FO definability results for forgetting a predicate. In fact, Doherty et al. [2001] used such techniques for computing strongest necessary and weakest sufficient conditions of FO formulas, which are concepts closely related to forgetting. As surveyed in [Nonnengart et al., 1999], the following is a classical result on second-order quantifier elimination due to Ackermann (1935). A formula φ is positive (resp. negative) wrt a predicate P if ¬P (resp. P) does not occur in the negation normal form of φ.

Theorem 2.7 Let P be a predicate variable, and let φ and ψ(P) be FO formulas such that ψ(P) is positive wrt P and φ contains no occurrence of P at all. Then

is logically equivalent to ψ(P(⃗x) ← φ(⃗x)), denoting the result of replacing each occurrence of P(⃗t) in ψ with φ(⃗t), and similarly if the sign of P is switched and ψ is negative wrt P .

2.2 Basic action theories

The language Lsc of the situation calculus [Reiter, 2001] is a many-sorted first-order language suitable for describing dynamic worlds. There are three disjoint sorts: action for actions, situation for situations, and object for everything else. Lsc has the following components: a constant S0 denoting the initial situation; a binary function do(a, s) denoting the successor situation to s resulting from performing action a; a binary predicate P oss(a, s) meaning that action a is possible in situation s; action functions, e.g., move(x, y); a finite number of relational fluents, i.e., predicates taking a situation term as their last argument, e.g., ontable(x, s); and a finite number of situation-independent predicates and functions. For simplicity of presentation, we do not consider functional fluents in this paper.

Often, we need to restrict our attention to formulas that refer to a particular situation. For this purpose, we say that a formula φ is uniform in a situation term τ, if φ does not mention any other situation terms except τ , does not quantify over situation variables, and does not mention Poss.

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

1. Σ is the set of the foundational axioms for situations.
2. Dap is a set of action precondition axioms.
3. Dss is a set of successor state axioms (SSAs), one for each fluent, of the form

where γ+ F (⃗x, a, s) and γF (⃗x, a, s) are uniform in s.

1. Duna is the set of unique names axioms for actions: A(⃗x) ̸= A′ (⃗y), and A(⃗x) = A(⃗y) ⊃ ⃗x = ⃗y, where A and A′ are distinct action functions.
2. DS0 , usually called the initial database, is a finite set of sentences uniform in S0. We call DS0 the initial KB.

2.3 Progression

Lin and Reiter [1997] formalized the notion of progression. Let D be a basic action theory, and α a ground action. We denote by Sα the situation term do(α, S0).

Definition 2.8 Let M and M ′ be structures with the same domains for sorts action and object. We write M ∼Sα M ′ if the following two conditions hold: (1) M and M ′ interpret all situation-independent predicate and function symbols identically. (2) M and M ′ agree on all fluents at Sα: For every relational fluent F, and every variable assignment σ, M, σ |= F(⃗x, Sα) iff M ′ , σ |= F(⃗x, Sα).

We denote by L2sc the second-order extension of Lsc. The notion of uniform formulas carries over to L2sc .

Definition 2.9 Let DSα be a set of sentences in L2sc uniform in Sα. DSα is a progression of the initial KB DS0 wrt α if for any structure M, M is a model of DSα iff there is a model M ′ of D such that M ∼Sα M ′ .

Lin and Reiter [1997] proved that progression is always second-order definable. They used an old version of SSAs in their formulation of the result; here we reformulate their result using the current form of SSAs.

We let Dss[α, S0] denote the instantiation of Dss wrt α and S0, i.e., the set of sentences F (⃗x, do(α, S0)) ≡ ΦF (⃗x, α, S0). Let F1, . . . , Fn be all the fluents. We introduce n new predicate symbols P1, . . . , Pn. We use φ↑S0 to denote the result of replacing every occurrence of Fi(⃗t, S0) in φ by Pi(⃗t). We call Pi the lifting predicate for Fi. When Σ is a finite set of formulas, we denote by ∧Σ the conjunction of its elements.

Theorem 2.10 The following is a progression of DS0 wrt α:

where R1, . . ., Rn are second-order predicate variables.

Therefore, by Theorem 2.6, if φ is uniform in Sα and φ is a result of forgetting the lifting predicates ⃗ P in ∧(Duna ∪ DS0 ∪Dss[α, S0])↑S0, then it is a progression of DS0 wrt α.

3 Progression for local-effect actions

In this section, we show that for local-effect actions, progression is always FO-definable and computable.

We first show an intuitive result concerning forgetting a predicate: if a sentence φ entails that the truth values of two predicates P and Q are different at only a finite number of certain instances, then forgetting the predicate Q in φ can be obtained from forgetting the Q atoms of these instances in φ and then replacing Q by P in the result.

Let ⃗x be a variable vector, and let Δ = {⃗t1, . . . ,⃗tm} be a set of vectors of ground terms, where all the vectors have the same length. We use ⃗x ∈ Δ to denote the formula ⃗x = ⃗t1 ∨ . . . ∨ ⃗x = ⃗tm. Let P and Q be two predicates. We let Q(Δ) denote the set {Q(⃗t) | ⃗t ∈ Δ}, and we let P ≈Δ Q denote the sentence ∀⃗x.⃗x ̸∈ Δ ⊃ P (⃗x) ≡ Q(⃗x).

Proposition 3.1 Let φ be a formula, M |= P ≈Δ Q, and θ ∈ M(Q(Δ)). Then for any variable assignment σ, M, σ |= φ[θ](Q/P) iff M, σ |= φ[θ].

Theorem 3.2 Let P and Q be two predicates, and Δ a finite set of vectors of ground terms. If forget(φ,Q(Δ)) ⇔ψ, then forget(φ ∧ (P ≈Δ Q), Q) ⇔ ψ(Q/P ).

Proof: Let Γ = Q(Δ). By Theorem 2.4, forget(φ, Γ) ⇔ ∨θ∈M(Γ) φ[θ]. Let M be a structure. We show that M |= ∨θ∈M(Γ) φ[θ](Q/P ) iff there is a model M ′ of φ∧(P ≈ΔQ) s.t. M ∼Q M ′ . Suppose the latter. Let θ ∈ M(Γ) s.t. M ′ |= θ. Since M ′ |= θ and M ′ |= φ, by Proposition 2.3, M ′ |= φ[θ]. Since M ′ |= P ≈Δ Q, by Proposition 3.1, M ′ |= φ[θ](Q/P). Since M ∼Q M ′ , M |= φ[θ](Q/P).

Now suppose M |= φ[θ](Q/P), where θ ∈ M(Γ). Let M ′ be the structure s.t. M ∼Q M ′ , M ′ |= P ≈Δ Q, and M ′ |= θ. Since M ∼Q M ′ and M |= φ[θ](Q/P), M ′ |=φ[θ](Q/P). SinceM ′ |= P ≈Δ Q, by Proposition 3.1, M ′ |= φ[θ]. Since M ′ |= θ, by Proposition 2.3, M ′ |= φ.

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, s), then ⃗ d is contained in ⃗c . This contrasts with actions having non-local effects such as moving a briefcase, which will also move all the objects inside the briefcase without having mentioned them.

Definition 3.3 An SSA is local-effect if both γ+ F (⃗x, a, s) and γF (⃗x, a, s) are disjunctions of formulas of the form ∃⃗z [a = A(⃗u) ∧ φ(⃗u, s)], where A is an action function, ⃗u contains ⃗x, ⃗z is the remaining variables of ⃗u, and φ is called a context formula. An action theory is local-effect if each SSA is localeffect.

Example 3.1 Consider a simple blocks world. We use a single action, move(x, y, z), moving a block x from block y to block z. We use two 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. Clearly, the following SSAs are local-effect:

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

where ⃗ti is a vector of ground terms contained in ⃗t, and ψi(s) is a formula whose only free variable is s. Without loss of generality, we assume that for a local-effect SSA, γ+ F (⃗x, α, s) and γF (⃗x, α, s) have the above simplified form. In the case of our blocks world, we have:

Following Vassos et al. [2008], we define the concepts of argument set and characteristic set:

Definition 3.4 Let D be local-effect, and α a ground action. The argument set of fluent F wrt α is the following set:

The characteristic set of α is the following set of atoms:

We let Dss[Ω] denote the instantiation of Dss wrt Ω, i.e., the set of sentences F(⃗t, Sα) ≡ ΦF (⃗t, α, S0), where F(⃗t, s) ∈ Ω. We let Dss[Ω] denote the set of sentences ⃗x ̸∈ ΔF ⊃ F (⃗x, Sα) ≡ F (⃗x, S0). Then we have

Proposition 3.5 Let D be local-effect, and α a ground action. Then Duna |= Dss[α, S0] ≡ Dss[Ω] ∪ Dss[Ω].

Theorem 3.6 Let D be local-effect, and α a ground action. Let Ω(s) be the characteristic set of α. Then the following is a progression of DS0 wrt α:

Proof: By Proposition 3.5, Theorems 2.4, 2.10 and 3.2.

The size of the progression is O(2mn), where m is the size of the characteristic set, and n is the size of the action theory. When we do iterative progression wrt a sequence δ of actions, the size of the resulting KB is O(2lmn), where l is the length of δ, and m is the maximum size of the characteristic sets.

Corollary 3.7 Progression for local-effect actions is always FO definable and computable.

We remark that this result is strictly more general than the one obtained by Vassos et al. [2008], who only showed that progression for local-effect actions is FO definable in a nonconstructive way, i.e., they left open the question whether the FO representation is computable or even finite. Moreover, while their proof is quite involved, having to appeal to Compactness of FO logic, ours is actually fairly simple.

Example 3.1 continued. Let α = move(A, B, C). Then Ω = {clear(B, s), clear(C, s), on(A, B, s), on(A, C, s), eh(A, s)}. Dss[Ω] is simplified to {clear(B, Sα), ¬clear(C, Sα), ¬on(A,B,Sα), on(A,C,Sα), eh(A,Sα)≡¬eh(C, S0)}.

Let DS0 be the following set of sentences: A ̸= B, A ̸= C, B ̸= C, clear(A, S0), on(A, B, S0), clear(C, S0), clear(x, S0) ⊃ eh(x, S0), on(x, y, S0) ⊃ ¬clear(y, S0).

Then DS0 entails ϑ, denoting ¬clear(B, S0)∧clear(C, S0)∧ on(A, B, S0) ∧ ¬on(A, C, S0). Thus there are only two θ ∈ M(Ω(S0)) which are consistent with DS0 :

θ1 = ϑ ∧ eh(A, S0) and θ2 = ϑ ∧ ¬eh(A, S0).

For example, let φ = clear(x, S0) ⊃ eh(x, S0). Then φ[θ1] ⇔ clear(x, S0)[ϑ] ⊃ x = A∨x ̸= A∧eh(x, S0), and φ[θ2] ⇔ clear(x, S0)[ϑ] ⊃ x ̸= A ∧ eh(x, S0). Thus φ[θ1] ∨ φ[θ2] is equivalent to

By Theorem 3.6 and Corollary 2.5, the following is a progression of DS0 wrt α:

move(x1, y1, z1) = move(x2, y2, z2)

⊃ x1 = x2 ∧ y1 = y2 ∧ z1 = z2,

A ̸= B, A ̸= C, B ̸= C, clear(A, Sα),

x = C ∨ x ̸= B ∧ x ̸= C ∧ clear(x, Sα) ⊃

x = A ∨ x ̸= A ∧ eh(x, Sα),

x = A∧ y = B ∨

(x ̸= A ∨ y ̸= B) ∧ (x ̸= A ∨ y ̸= C) ∧ on(x, y, Sα) ⊃

¬(y = C ∨ y ̸= B ∧ y ̸= C ∧ clear(y, Sα)),

clear(B, Sα), ¬clear(C, Sα), ¬on(A, B, Sα),

on(A, C, Sα), eh(A, Sα) ≡ ¬eh(C, Sα).

4 Progression for normal actions

In the last section, we showed that for local-effect actions, progression is FO definable and computable. An interesting observation about non-local-effect actions is that their effects often do not depend on the fluents on which they have nonlocal effects, that is, they normally have local effects on the fluents that appear in every γ+ F and γF . For example, moving a briefcase will move all the objects in it as well without affecting the fluent in. We will call such an action a normal action. In this section, we show that for a normal action α, if the initial KB has the property that for each fluent F on which α has non-local effects, the only appearance of F is in the form of φ(⃗x) ⊃ F(⃗x, S0) or φ(⃗x) ⊃ ¬F(⃗x, S0), then progression is FO definable and computable.

Our result is inspired by a result by Lin and Reiter [1997] that for context-free action theories, that is, action theories where every predicate appearing in every γ+ F and γF is situation-independent, if the initial KB has the property that for each fluent F, the only appearance of F is in the form of φ(⃗x) ⊃ F(⃗x, S0) or φ(⃗x) ⊃ ¬F(⃗x, S0), then progression is FO definable and computable. Incidentally, their result can be considered as an application of a simple case of the classical result by Ackermann (see Theorem 2.7). To prove our result, we combine the application of this simple case and the proof idea behind our result for local-effect actions.

We first present this simple case of Ackermann's result:

Definition 4.1 We say that a finite theory T is semidefinitional wrt a predicate P if the only appearance of P in T is in the form of P(⃗x) ⊃ φ(⃗x), where we call φ(⃗x) a necessary condition of P, or φ(⃗x) ⊃ P(⃗x), where we call φ(⃗x) a sufficient condition of P . We use WSCP (meaning weakest sufficient condition) to denote the disjunction of φ(⃗x) such that φ(⃗x) ⊃ P(⃗x) is in T, and we use SNCP (meaning strongest necessary condition) to denote the conjunction of φ(⃗x) such that P(⃗x) ⊃ φ(⃗x) is in T .

Theorem 4.2 Let T be finite and semi-definitional wrt P . Let T ′ be the set of sentences in T that contains no occurrence of P . Then forget(T, P ) ⇔ T ′ ∧ ∀⃗x.WSCP (⃗x) ⊃ SNCP (⃗x).

Proof: Clearly, ∃R.T(P/R) |= T ′ ∧ ∀⃗x.WSCP (⃗x) ⊃ SNCP (⃗x). To prove the opposite entailment, simply use the definition ∀⃗x.P (⃗x) ≡ WSCP (⃗x).

The following proposition shows that the SSA for a fluent F is semi-definitional wrt the predicate F(⃗x, S0) provided that F does not appear in γ+ F or γF .

Proposition 4.3 The sentence F(⃗x, Sα) ≡ γ+ F (⃗x, α, S0) ∨ F (⃗x, S0) ∧ ¬γF (⃗x, α, S0) is equivalent to the following sentences: ¬γ+ F ∧ F(⃗x, Sα) ⊃ F(⃗x, S0), F(⃗x, S0) ⊃ γF ∨ F(⃗x, Sα), γ+ F ⊃ F(⃗x, Sα), and ¬γ+ F ∧ γF ⊃ ¬F(⃗x, Sα).

We now formalize our constraints on the actions and the initial KBs.

Definition 4.4 We say that a ground action α has local effects on a fluent F , if by using Duna, each of γ+ F (⃗x, α, s) and γF (⃗x, α, s) can be simplified to a disjunction of formulas of the form ⃗x = ⃗t∧ψ(s), where ⃗t is a vector of ground terms, and ψ(s) is a formula whose only free variable is s. We denote by LE(α) the set of all fluents on which α has local effects.

Definition 4.5 We say that α is normal if for each fluent F, all the fluents that appear in γ+ F and γF are in LE(α).

Clearly, both context-free and local-effect actions are normal actions.

Definition 4.6 We say that DS0 is normal wrt α if for each fluent F ̸∈ LE(α), DS0 is semi-definitional wrt F.

Thus any fluent F ∈ LE(α) can appear in DS0 in an arbitrary way. We now have the main result of this section:

Theorem 4.7 Let DS0 be normal wrt a normal action α. Then progression of DS0 wrt α is FO definable and computable.

Proof: By Theorem 2.10, we need to forget the lifting predicates in ∧(Duna ∪ DS0 ∪ Dss[α, S0]) ↑ S0. Since α is normal, for each fluent F, all the fluents that appear in γ+ F and γF are in LE(α). By Proposition 4.3, for each F ̸∈ LE(α), Dss[α, S0] is semi-definitional wrt F(⃗x, S0). Since DS0 is normal wrt α, for each fluent F ̸∈ LE(α), DS0 is semidefinitional wrt F. By applying Theorem 4.2, we forget the lifting predicate for F ̸∈ LE(α). Now by applying Theorem 3.6, we forget the lifting predicate for F ∈ LE(α).

Example 4.1 The following is Dss for the briefcase domain: at(x, l, do(a, s)) ≡ (∃b)[a = move(b, l)∧(x = b∨in(x, b, s))]∨ at(x, l, s) ∧ ¬(∃b, m)[a = move(b, m) ∧ (x = b ∨ in(x, b, s))], in(x, b, do(a, s)) ≡ a = putin(x, b) ∨

For a ground action α = move(c1, c2), by using Duna,

Dss[α, S0] can be simplified as follows: at(x, l, do(α, S0)) ≡ l = c2 ∧ (x = c1 ∨ in(x, c1, S0)) ∨

in(x, b, do(α, S0)) ≡ in(x, b, S0).

Clearly, α has local effects on in, and it is a normal action.

Now let DS0 be as follows:

∃x∀y¬in(x, y, S0), ¬in(A1, B1, S0),

in(A2, B2, S0) ∨ in(A2, B3, S0),

at(b, l, S0) ∧ in(x, b, S0) ⊃ at(x, l, S0),

at(x, l′ , S0) ∧ l ̸= l′ ⊃ ¬at(x, l, S0),

b = B1 ∧ l = L1 ∨ b = B2 ∧ l = L2 ⊃ at(x, l, S0),

b = B3 ∧ (l = L1 ∨ l = L2) ⊃ ¬at(x, l, S0).

Then DS0 is normal wrt α = move(B1,L2). To progress it wrt α, we first apply Theorem 4.2 to forget the lifting predicate for at(x, l, s), and obtain a set Σ of sentences as follows:

1. If φ ∈ DS0 does not mention fluent at, then φ ∈ Σ.
2. Add to Σ the following sentences: l = L2 ∧ (x = B1 ∨ in(x, B1, S0)) ⊃ at(x, l, Sα), l ̸= L2 ∧ (x = B1 ∨ in(x, B1, S0)) ⊃ ¬at(x, l, Sα).
3. If φ ⊃ at(x, l, S0) is in DS0 , then add to Σ the sentence φ ∧ ¬(x = B1 ∨ in(x, B1, S0)) ⊃ at(x, l, Sα).
4. If φ ⊃ ¬at(x, l, S0) is in DS0 , add to Σ the sentence φ∧(l ̸= L2∨x ̸= B1∧¬in(x, B1, S0)) ⊃ ¬at(x, l, Sα).

Now since we have in(x, b, Sα) ≡ in(x, b, S0), we simply replace each occurrence of S0 in Σ with Sα; the result together with Duna is a progression of DS0 wrt α.

5 Progression of proper+ KBs

In Sections 3 and 4, we showed that for local-effect and normal actions, progression is FO definable and computable. However, the progression may not be efficiently computable.

In this section, we show that for local-effect and normal actions, progression is not only FO definable but also efficiently computable under the two constraints that the initial KB is in the form of the so-called proper+ KBs, which represent firstorder disjunctive information, and the successor state axioms are essentially quantifier-free.

Proper+ KBs were proposed by Lakemeyer and Levesque [2002] as a generalization of proper KBs, which were proposed by Levesque [1998] as an extension of databases. Intuitively, a proper+ KB is equivalent to a (possibly infinite) set of ground clauses. A tractable limited reasoning service has been developed for proper+ KBs [Liu et al., 2004; Liu and Levesque, 2005]. What is particularly interesting about our results here is that progression of proper+ KBs is definable as proper+ KBs, so that we can make use of the available tractable reasoning service.

To formally define proper+ KBs, we use a FO language Lc with equality, a countably infinite set of constants, which are intended to be unique names, and no other function symbols. We let e range over ewffs, i.e., quantifier-free formulas whose only predicate is equality. We denote by E the axioms of equality and the set of formulas {(c ̸= c′ ) | c and c′ are distinct constants}. We let ∀φ denote the universal closure of φ.

Definition 5.1 Let e be an ewff and d a clause. Then a formula of the form ∀(e ⊃ d) is called a ∀-clause. A KB is called proper+ if it is a finite non-empty set of ∀-clauses.

Example 5.1 Consider our blocks world. The following is a initial KB DS0 which is proper+:

on(x, y, S0) ⊃ ¬clear(y, S0),

on(x, y, S0) ∧ eh(y, S0) ⊃ ¬eh(x, S0),

x = A ∨ x = C ⊃ clear(x, S0),

x = D ∨ x = E ∨ x = F ⊃ ¬eh(x, S0),

x = A ∧ y = B ∨ x = B ∧ y = F ⊃ on(x, y, S0),

on(C, D, S0) ∨ on(C, E, S0).

We begin with forgetting in proper+ KBs. We first introduce some definitions and propositions.

Definition 5.2 Let φ be a sentence, and p a ground atom. We say that p is irrelevant to φ if forget(φ, p) ⇔ φ.

Proposition 5.3 Let p be a ground atom. Let φ1, φ2, φ3 be sentences such that p is irrelevant to them. Then forget((φ1 ⊃ p) ∧ (p ⊃ φ2) ∧ φ3, p) ⇔ (φ1 ⊃ φ2) ∧ φ3.

Proposition 5.4 Let φ = ∀(e ⊃ d) be a ∀-clause, and P(⃗c) a ground atom. Suppose that for any P(⃗t) appearing in d, e ∧⃗t = ⃗c is unsatisfiable. Then P(⃗c) is irrelevant to φ.

Definition 5.5 Let Σ be a proper+ KB, and P(⃗c) a ground atom. We say that Σ is in normal form wrt P(⃗c), if for any ∀(e ⊃ d) ∈ Σ, and for any P(⃗t) appearing in d, either ⃗t is ⃗c or e ∧ ⃗t = ⃗c is unsatisfiable.

Proposition 5.6 Let P(⃗c) be a ground atom. Then every proper+ KB can be converted into an equivalent one which is in normal form wrt P(⃗c). This can be done in O(n+2wm) time, where n is the size of Σ, m is the size of sentences in Σ where P appears, and w is the maximum number of appearances of P in a sentence of Σ.

Proof: Let φ = ∀(e ⊃ d) be a ∀-clause. Let P (⃗t1), . . ., P (⃗tk) be all the appearances of P in φ, and let Θ={∧ki=1 ⃗ti ◦i ⃗c | ◦i ∈ {=, ̸=}}. Let θ ∈ Θ. We let d[θ] denote d with each P(⃗ti), 1 ≤ i ≤ k, replaced by P(⃗c) if θ contains ⃗ti = ⃗c. We use φ[θ] to denote ∀(e ∧ θ ⊃ d[θ]). Obviously, φ is equivalent to the theory {φ[θ] | θ ∈ Θ}, which we denote by NF(φ, P(⃗c)). For a proper+ KB Σ, we convert it into the union of NF(φ, P (⃗c)) where φ ∈ Σ.

In the above proof, we can remove those generated ∀- clauses ∀(e ⊃ d) where d contains complemental literals or e is unsatisfiable wrt E. For example, the ewff x = y ∧ x = A ∧ y = B is unsatisfiable wrt E. Also, a ∀-clause ∀(e ∧ t = c ⊃ d) can be simplified to ∀(e ⊃ d)(t/c). Finally, an ewff can be simplified by use of E.

Definition 5.7 Let φ1 = ∀(e1 ⊃ d1∨P (⃗t)) and φ2 = ∀(e2 ⊃ d2 ∨¬P (⃗t)) be two ∀-clauses, where ⃗t is a vector of constants or a vector of distinct variables. Without loss of generality, we assume that φ1 and φ2 do not share variables other than those contained in ⃗t. We call the ∀-clause ∀(e1 ∧ e2 ⊃ d1 ∨ d2) the ∀-resolvent of the two input clauses wrt P(⃗t).

Theorem 5.8 Let Σ be a proper+ KB, and P(⃗c) a ground atom. Then the result of forgetting P(⃗c) in Σ is definable as a proper+ KB and can be computed in O(n + 4wm2 ) time, where n, w, and m are as above.

Proof: We first convert Σ into normal form wrt P(⃗c). Then we compute all ∀-resolvents wrt P(⃗c) and remove all clauses with P(⃗c). This results in a proper+ KB, which, by Propositions 5.3 and 5.4, is a result of forgetting P(⃗c) in Σ.

Theorem 5.9 Let Σ be a proper+ KB which is semidefinitional wrt predicate P. Then the result of forgetting P in Σ is definable as a proper+ KB and can be computed in O(n +m2 ) time, where n is the size of Σ, and m is the size of sentences in Σ where P appears.

Proof: We compute all ∀-resolvents wrt P(⃗x) and remove all clauses containing P(⃗x). This results in a proper+ KB, which, by Theorem 4.2, is a result of forgetting P in Σ.

In the above theorems (Theorems 5.8 and 5.9), it is reasonable to assume that w = O(1) and m2 = O(n). Under this assumption, both forgetting can be computed in O(n) time.

Based on the above theorems, we have the following results concerning progression of proper+ KBs. We first introduce a constraint on successor state axioms.

Definition 5.10 An SSA is essentially quantifier-free if for each ground action α, by using Duna, each of γ+ F (⃗x, α, s) and γF (⃗x, α, s) can be simplified to a quantifier-free formula.

For example, the SSAs for our blocks world and briefcase examples are essentially quantifier-free. For a local-effect SSA, if each context-formula is quantifier-free, then it is essentially quantifier-free. In general, if both γ+ F (⃗x, a, s) and γF (⃗x, a, s) are disjunctions of formulas of the form ∃⃗z [a = A(⃗u) ∧ φ(⃗x, ⃗z, s)], where ⃗u contains ⃗z, and φ is quantifierfree, then the SSA is essentially quantifier-free.

Proposition 5.11 Suppose Dss is essentially quantifier-free. Then Dss[α, S0] is definable as a proper+ KB.

• Theorem 5.12 Suppose that D is local-effect, Dss is essentially quantifier-free, and DS0 is proper+. Then progression of DS0 wrt any ground action α is definable as a proper+ KB and can be efficiently computed.

Theorem 5.13 Suppose that Dss is essentially quantifierfree, α is a normal action, and DS0 is a proper+ KB which is normal wrt α. Then progression of DS0 wrt α is definable as a proper+ KB and can be efficiently computed.

Example 5.1 continued. We now progress DS0 wrt α = move(A,B,C). For simplicity, we remove the second sentence from DS0 . The characteristic set of α is Ω = {clear(B, s), clear(C, s), on(A, B, s), on(A, C, s), eh(A, s)}. Dss[Ω] is simplified to the following proper+ KB:

{clear(B, Sα), ¬clear(C, Sα), ¬on(A, B, Sα), on(A, C, Sα), eh(A, Sα) ∨ eh(C, S0), ¬eh(A, Sα) ∨ ¬eh(C, S0)}.

We convert DS0 into normal form wrt Ω(S0), and obtain after simplification:

• y ̸= B ∧ y ̸= C ∧ (x ̸= A ∨ y ̸= B ∧ y ̸= C) ⊃ (on(x, y, S0) ⊃ ¬clear(y, S0)),

x ̸= A ⊃ (on(x, B, S0) ⊃ ¬clear(B, S0)),

x ̸= A ⊃ (on(x, C, S0) ⊃ ¬clear(C, S0)),

on(A, B, S0) ⊃ ¬clear(B, S0),

on(A, C, S0) ⊃ ¬clear(C, S0),

x = D ∨ x = E ∨ x = F ⊃ ¬eh(x, S0),

clear(A, S0), clear(C, S0), on(A, B, S0), on(B, F, S0), on(C, D, S0) ∨ on(C, E, S0).

We now do resolution on DS0 ∪Dss[Ω] wrt atoms in Ω(S0), delete all clauses with some atom from Ω(S0), and obtain the following set Σ:

clear(B, Sα), ¬clear(C, Sα), ¬on(A, B, Sα), on(A, C, Sα), eh(A, Sα) ∨ eh(C, S0), ¬eh(A, Sα) ∨ ¬eh(C, S0),

y ̸= B ∧ y ̸= C ∧ (x ̸= A ∨ y ̸= B ∧ y ̸= C) ⊃

(on(x, y, S0) ⊃ ¬clear(y, S0)),

x ̸= A ⊃ ¬on(x, C, S0),

x = D ∨ x = E ∨ x = F ⊃ ¬eh(x, S0),

clear(A, S0), on(B, F, S0), on(C, D, S0) ∨ on(C, E, S0).

We replace every occurrence of S0 in Σ with Sα; the result together with Duna is a progression of DS0 wrt α.

6 Conclusions

In this paper, we have presented the following results. First, we showed that for local-effect actions, progression is FO definable and computable. This result is stronger than the one obtained by Vassos et al. [2008], and our proof is a very simple one via the concept of forgetting. Next, we went beyond local-effect actions, and showed that for normal actions, i.e., actions whose effects do not depend on the fluents on which the actions have non-local effects, if the initial KB is semidefinitional wrt these fluents, progression is FO definable and computable. Third, we showed that for local-effect actions whose successor state axioms are essentially quantifier-free, progression of proper+ KBs is definable as proper+ KBs and can be efficiently computed. Thus we can utilize the available tractable limited reasoning service for proper+ KBs. As an extension of our first result, we have shown that for finiteeffect actions, which change the truth values of fluents at only a finite number of instances, progression is FO definable. We have also shown that in the presence of functional fluents, our first and second results still hold. For lack of space, these results will be presented in a longer version of the paper. For the future, we would like to implement a Golog interpreter based on progression of proper+ KBs, which we expect will lead to a more efficient version of Golog compared to the current implementation based on regression.

Acknowledgments

We thank the anonymous reviewers for very helpful comments. This work was supported in part by the European Union Erasmus Mundus programme.