First-Order Progression beyond Local-Effect and Normal Actions

1 Introduction

In reasoning about action and change, projection is perhaps the most fundamental problem. Given a sequence of actions and a target formula, the task is to determine whether the formula comes to hold after executing the action sequence. Typically, the domain in question is represented through an action theory that includes, among other things, a knowledge base (KB) describing the initial state of the world, as well as axioms encoding the pre- and post-conditions of actions. There are at least two different approaches to projection: On the one hand, there is regression, where one transforms the formula backward into an equivalent one about the initial situation, and then checks whether that formula holds according to the initial KB. Conversely, in progression, one updates the initial KB to reflect the changes brought about by the action sequence and then determines whether the goal formula is entailed. In the well-studied Situation Calculus [McCarthy and Hayes, 1969; Reiter, 2001] formalism, regression is very straightforward. However, in practice, it very quickly becomes unfeasible, as the resulting formula can grow exponentially in size (unless one introduces new fluents as in [van Ditmarsch et al., 2007]), which is particularly problematic the longer the action sequence gets. One benefit of progression is that one only has to progress the KB once, and can then check multiple queries against it. However, the problem of computing a progression for a given action and KB is notoriously challenging: A strong negative result due to Lin and Reiter [1997] is that in general, the progression of a first-order theory may require second-order logic. Vassos and Levesque [2008] later showed that the second-order nature is inescapable in the sense that even when allowing for infinite theories, a restriction to first-order theories is strictly weaker.

Efforts have been made to identify restricted classes of theories, where first-order definability can be guaranteed. In their seminal work, Lin and Reiter presented such results for so-called relatively complete theories, where the initial KB has complete knowledge about the state of the world, and context-free theories, where action effects are limited to adding and deleting ground literals as in the classical STRIPS [Fikes and Nilsson, 1971] planning language. Liu and Lakemeyer [2009], extending earlier work due to Vassos et al. [2008], later showed the existence of a first-order progression for a less restricted class of theories, namely where actions only have local effects. Intuitively, this means that actions must mention all affected objects explicitly in their arguments. For example, an action move(x, y, z) for moving a block x from y to z only affects the truth of on(x, y) and on(x, z). Classical examples of actions that are not localeffect include moving a briefcase, which moves all (unmentioned) contained items along with it, and exploding a bomb, which destroys all (unmentioned) objects in its vicinity. To capture such domains, Liu and Lakemeyer [2009] generalized the result on local-effect actions to so-called normal actions, which allow for non-local effects, as long as the affected fluent predicates only depend on ones that are themselves only subject to local effects, under certain conditions to the initial KB. They also showed that for certain types of KB, called proper+ [Lakemeyer and Levesque, 2002], progression is computationally efficient.

An example that goes beyond what is expressable by means of normal actions, and that is hence not supported by Liu and Lakemeyer's results, is when objects contained in a box that is on a shelf become broken from dropping the box. Here, broken is a non-local-effect predicate that depends on another non-local-effect predicate, nameley on. In this paper, we show that for a class of actions that includes such scenarios, and that strictly subsumes that of normal actions, progression is also first-order definable. In such action theories, called acyclic, dependencies between non-local effect fluent predicates are allowed, as long as they do not contain any cycles. We also show that progression is efficient under reasonable assumptions, where dependencies among fluents do not introduce significant additional complexity.

The remainder of the paper is organized as follows. The following section presents formal preliminaries about action theories and progression and reviews the first-order progression result on local-effect actions and normal actions by Liu and Lakemeyer [2009]. Our results on progression of the more general class of acyclic theories are presented in Section 3. We then go on to provide computability results in Section 4, after which we discuss related work and conclude.

2 Preliminaries

In this section, we review progression in the Situation Calculus and the result on local-effect and normal actions by [Liu and Lakemeyer, 2009].

We start with a first-order (FO) language L with equality. For simplicity, we only consider predicates and ignore functions. The set of formulas of L is the least set that 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. For readability, we will use parentheses around quantifiers to indicate the scopes, and "dot" to indicate that the quantifier preceding the dot has maximum scope, e.g., ∀x.ϕ(x) ⊃ ψ(x) stands for ∀x(ϕ(x) ⊃ ψ(x)). Leading universal quantifiers might be omitted in writing sentences, i.e., we assume that free variables are implicitly ∀-quantified from the outside. E.g., we identify ϕ(x) with ∀x.ϕ(x). We use ψ ⇔ ψ to mean ϕ and ψ are logically equivalent. Let ψ be a formula, and let µ and µ′ be two expressions (terms or formulas). We denote by ϕ(µ/µ′ ) the result of simultaneously substituting every occurrence of µ in ϕ with µ′ .

2.1 Basic Action Theories

The situation calculus [Reiter, 2001] Lsc is a many-sorted language with some second-order (SO) features suitable for describing dynamic worlds. There are three sorts: action, situation, and object. Lsc contains the following features: a distinct constant S0 denoting the initial situation; a binary function do(a, s) deriving the resulting situation from doing action a in situation s; a binary relation Poss(a, s) expressing action a being executable in situation s; action functions, e.g. move(x, y); a finite set of fluent predicates, i.e., predicates whose last argument is a situation term.

A (possibly second-order) formula ϕ is uniform in a situation term s if ϕ does not mention any other situation terms except s, does not quantify over situation variables, and does not mention Poss .

The dynamics of a domain is specified by a basic action theory (BAT) in Lsc of the form

1. Σind is a set of domain-independent axioms that ensure situations are well-structured;
2. Dap is a set of action precondition axioms;
3. Dss is a set of successor state axioms (SSAs), one for each fluent predicate F, of the form

where γ+ F and γF are uniform in s. γ+ F and γF are the conditions under which the action causes F to become true and false, respectively;

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

Successor state axioms constitute Reiter's [1991] solution to the frame problem. In particular, it is required that for all fluent predicates F, D |= ¬(γ+ F ∧ γF ). Henceforth, given a ground action α, we use Sα to refer to the situation do(α, S0).

2.2 Progression

A progression should retain all proper information, i.e., logical entailments in terms of the future of the initial KB. The below definition by [Vassos and Levesque, 2013] formalizes this intuition, and it is equivalent to the original model-theoretical one by [Lin and Reiter, 1997].

Definition 1 (Progression). Let D be a basic action theory, α a ground action, and DSα a set of (first-order or second-order) sentences uniform in Sα. We say that DSα is a progression of DS0 wrt α, D iff for every sentence ϕ uniform in Sα,

Lin and Reiter [1997] proved that progression is always second-order definable. We write the instantiation of Dss wrt α and S0 as Dss[α, S0], i.e. Dss[α, S0] is the set of sentences F(⃗x, do(α, S0)) ≡ ΦF (⃗x, α, S0), where ΦF denotes the right-hand side of the SSA for F . Let F1, . . . Fn be the set of all fluents. For each fluent Fi, we introduce a new predicate symbol Pi. We use ϕ ↑ S0 to denote the result of replacing every Fi(⃗t, S0) in ϕ by Pi(⃗t) and call Pi the lifting predicate for Fi. For a finite set of formulas Σ, we also use Σ to denote the conjunctions of its elements. Using this notation, the following is a progression of DS0 wrt α:

where ⃗R = {R1, . . . , Rn} are SO predicate variables.

Efforts have been made to identify fragments of the Situation Calculus where progression is first-order definable, i.e. conditions under which Eq. (1) is equivalent to a first-order theory. For instance, [Lin and Reiter, 1997] showed that this is the case if the initial KB is relatively complete, i.e., for every sentence ϕ uniform in S0, KB entails either ϕ or its negation, or if the basic action theory is context-free, i.e. actions' effects are independent of situations. See also [Vassos and Patrizi, 2013] for a classification of FO definable KBs and action theories.

Local-Effect Actions

Liu and Lakemeyer [2009] (henceforth LL09) showed that if the basic action theory is local-effect, then progression is always FO definable. Intuitively, a ground action has local effects if it only affects the truth of ground fluent atoms that mention only the action's parameters. For example, an action move(x, y, z) for moving a block x from y to z only affects the truth of on(x, y) and on(x, z).

Definition 2. 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 the context. An action theory is local-effect if each SSA is local-effect.

The result in LL09 to progress local-effect action theories is based on forgetting [Lin and Reiter, 1994]. Intuitively, forgetting a ground atom (or predicate) in a theory leads to a weaker theory that entails the same set of sentences that are "irrelevant" to the atom (or predicate). Forgetting in propositional logic is equivalent to propositional existential quantification: the result of forgetting atom p from formula ϕ is ϕ(p/TRUE) ∨ ϕ(p/FALSE), where ϕ(p/TRUE) (resp. ϕ(p/FALSE)) denotes the result of replacing each occurrence of p in ϕ by TRUE (resp. FALSE). Forgetting a ground atom in an FO theory is more complicated but can be computed in a similar spirit; we refer interested readers to [Lin and Reiter, 1994]. Lastly, forgetting a predicate P in a theory T , written as forget(T, P), amounts to replacing the predicate with a SO variable and existentially quantifying it from the outside, i.e. ∃R.T(P/R). Progression as in Eq. (1) thus amounts to adding the effects of the action (Dss[α, S0]) and forgetting all lifting predicates of fluents (quantified existentially from the outside). LL09 observed that for a local-effect action theory, every ground action will affect only finitely many fluent atoms, the so-called characteristic set Ω, determined by the action's parameters. Hence, forgetting the lifting predicates can be reduced to forgetting these finitely many instances, resulting in a first-order theory. For space reasons, we do not go into details about how to compute such an FO progression by forgetting, but simply assume that we can apply the procedure described by LL09 when we need to forget local-effect fluents.

Normal Actions

Actions with global effects are ubiquitous, for example, exploding a bomb will destroy every fragile object in its vicinity. The inability of local-effect action theories to capture such dynamic domains motivated LL09 to propose a more general version of action theories that admit so-called normal actions. The idea is to allow non-local-effect fluents in a limited fashion. By imposing additional constraints on the initial KB and SSAs, a technique for SO quantifier elimination based on Ackermann's Lemma [1935] can be applied to forget the lifting predicates for those fluents.

Definition 3. A finite theory T is semi-definitional wrt a predicate P if the only occurrence of P in T is of the form P(⃗x) ⊃ ϕ(⃗x) or ψ(⃗x) ⊃ P(⃗x). ϕ (respectively ψ) is called a necessary (sufficient) condition of P .

Let WSCP (weakest sufficient condition) be the disjunction of formulas ψ(⃗x) such that ψ(⃗x) ⊃ P(⃗x) is in T, and SNCP (strongest necessary condition) be the conjunction of formulas ϕ(⃗x) with P (⃗x) ⊃ ϕ(⃗x) in T .

Theorem 1 ([Liu and Lakemeyer, 2009]). Let T be finite and semi-definitional wrt P, and T ′ the set of sentences in T not mentioning P . Then forget (T, P ) ⇔ T ′ ∧ ∀⃗x.WSCP (⃗x) ⊃ SNCP (⃗x).

This provides a means to eliminate the SO quantifiers introduced by forgetting a predicate.

Proposition 1. In any model of D, the sentence F(⃗x, Sα) ≡ γ+ F (⃗x, α, S0) ∨ ¬γF (⃗x, α, S0) ∧ F(⃗x, S0) is equivalent to the conjunction of following sentences: ¬γ+ F ∧ F(⃗x, Sα) ⊃ F(⃗x, S0), F(⃗x, S0) ⊃ γF ∨ F(⃗x, Sα), γ+ F ⊃ F(⃗x, Sα), and γF ⊃ ¬F(⃗x, Sα). 1

The proposition suggests that after lifting, SSAs are semidefinitional wrt the respective lifting predicates.

Definition 4. A ground action α is said to have local effects on a fluent F, if by using Duna, γ+ 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 ψ is a formula whose only free variable is s.

Let LE(α) be the set of fluents on which α has local effects and NLE(α) = {F | F is in D, and F /∈ LE(α)}, i.e., the set of remaining fluents.

Definition 5 (Normal Action). A ground action α is normal if for each fluent F, all the fluents that appear in γ+ F and γF are in LE(α).

Clearly, local-effect actions are normal actions. We say that DS0 is normal wrt α if DS0 is semi-definitional wrt each fluent in NLE(α).

Theorem 2 ([Liu and Lakemeyer, 2009]). Let DS0 be normal wrt a normal action α, then progression of DS0 wrt α is FO definable and computable.

Intuitively, this is because for such a theory D and action α, one can use Theorem 1 to forget the lifting predicates of fluents in NLE(α), and thereafter use the techniques for localeffect theories to forget lifting predicates for fluents in LE(α).

Example 1. Consider the domain that is described by the two fluents broken(x, s) and shielded(x, s) that say, respectively, that object x is broken and shielded in situation s. The action explode will destroy everything that is unshielded. The following BAT expresses such a domain:

1 The proposition is almost identical to Proposition 4.3 of LL09, the only difference being that they use ¬γ+ F ∧ γF ⊃ ¬F(⃗x, Sα) instead of γF ⊃ ¬F(⃗x, Sα). Our simplification is justified by the assumption that D |= ¬(γ+ F ∧ γF ).

broken(x, do(a, s)) ≡ a = explode ∧ ¬shielded(x, s) ∨ broken(x, s) shielded(x, do(a, s)) ≡ shielded(x, s)

Clearly, the ground action α = explode has local effects on shielded (in fact it has no effects on shielded at all) and it is a normal action with broken ∈ NLE(α).

Let DS0 be {broken(x, S0) ⊃ x = A}, then DS0 is normal wrt explode. Grounding Dss wrt explode and applying Prop. 1, we obtain

{ shielded(x, S0) ∧ broken(x, Sα) ⊃ broken(x, S0), broken(x, S0) ⊃ broken(x, Sα), ¬shielded (x, S0) ⊃ broken(x, Sα) }

Applying Theorem 1 to forget the lifting predicate for broken(x, S0) and substituting S0 by Sα, we obtain

3 Progressing Acyclic Actions

Although the class of normal actions is capable of capturing the phenomenon of global effects, the requirement that for each fluent F, fluents in γ+ F and γF have to be local-effect is a limitation. Among other things, it disallows a non-localeffect fluent to depend on other non-local-effect fluents. In this section, we lift this limitation and show that first-order definability preserves for a more general class of actions, i.e. acyclic actions, where non-local-effect fluents can interact in a complex manner as long as the dependency among fluents does not contain cycles. Intuitively, for such actions, one can use Theorem 1 to iteratively forget the lifting predicates of non-local-effect fluents, following the order of fluent dependencies. Additional syntactical conditions on the SSAs guarantee that after each such step, the resulting KB is in the right form to apply Theorem 1 again.

To begin with, we broaden the class of formulas that can be handled by considering formulas that can be equivalently transferred into a semi-definitional form. Note that it is in general undecidable to determine if a formula is equivalent to a one in semi-definitional form wrt a predicate.

Definition 6. A formula ϕ(⃗x) is said to be in good form wrt a predicate P if it is of the form

where ψ, ψ′ , ψ′′ contains no P, and terms in ⃗t are either ground terms or free variables among ⃗x.

Proposition 2. If ϕ(⃗x) is in good form wrt a predicate P, then ¬ϕ(⃗x) can be rewritten in good form wrt P .

Lemma 1. If ϕ(⃗x) is in good form wrt a predicate P, then ϕ(⃗x) can be rewritten to be semi-definitional wrt P .

Proof. ϕ(⃗x) is equivalent to the set

The first sentence (likewise for the second) is equivalent to ∀⃗y.(∃⃗x. ⃗y = ⃗t ∧¬ψ(⃗x)) ⊃ P (⃗y). The third one is obvious as it does not mention P .

Definition 7. Given predicates ⃗ P = {P1, . . . , Pn}, a finite theory T is said to be separably semi-definitional wrt ⃗ P, if each sentence ϕi ∈ T mentions at most one predicate Pi ∈ ⃗ P and ϕi is semi-definitional wrt Pi.

Separably semi-definitional theories exclude formulas like Pi(⃗x) ⊃ Pj(⃗x) where both Pi, Pj are in ⃗ P .

Definition 8 (Dependency Graph). Given successor state axioms Dss and a ground action α, the dependency graph G of fluents in Dss wrt α is a directed graph defined as follows: (1) the vertices of G are the set of fluents; (2) there is an edge F → F ′ for two fluents F, F ′ iff F ∈ NLE(α) and F ′ appears in γ+ F or γF .

Definition 9 (Acyclic Action). A ground action α is acyclic (or has acyclic effects, or the BAT is acyclic wrt α) if

• its dependency graph G is acyclic; and
• for each fluent F, either all fluents in γ+ F and γF are in LE(α), or both γ+ F and γF are in good formwrt at most one fluent in NLE(α).

Theorem 3. Let α be an acyclic action, and DS0 be separably semi-definitional wrt NLE(α). Then the progression of DS0 wrt α is first-order definable and computable.

Proof. The non-trivial part lies in forgetting the lifting predicates for fluents in NLE(α). We define the depth of a fluent F in G as the length of the longest path starting in F.

We forget the lifting predicates in decreasing depth order. For a fluent F with maximal depth, lifting its instantiated SSA, we obtain (by Prop. 1)

Clearly, only Eq. (3a) and Eq. (3b) contain the lifting predicate P. Since DS0 is separably semi-definitional wrt NLE(α), forgetting P in {(Duna ∪DS0 ∪Dss[α, S0]) ↑ S0} is equivalent to replacing the formulas mentioning P in the lifted KB with the conjunction of formulas

where NCP (⃗x) is the conjunction of necessary conditions for P in DS0 ↑ S0, and SCP (⃗x) is the disjunction of sufficient conditions for P in DS0 ↑ S0. Note that by assumption both NCP (⃗x) and SCP (⃗x) contain no fluents in NLE(α).

By Prop. 2 and Lemma 1, the new formulas (4a)-(4c) together with (3c) and (3d) can all be transformed into a formula that is semi-definitional wrt at most one lifting predicate of a fluent in NLE(α). We add the transformed result to DS0 . Note the assumption that F has maximal depth guarantees that F is not mentioned in the resulting formulas, and so forgetting the remaining lifting predicates can be iterated.

contains

Figure 1: Dependency graph for BAT in Example 2.

Example 2. Consider a box domain with three fluents, adapted from [Claßen and Zarrieß, 2017]: contains(x, y, s) says that x contains y, on(x, y, s) says that x is on y, and broken(x, s) says that x is broken in situation s. Action drop(x, y) denotes dropping container x from shelf y, causing all things in x to become broken and no longer being positioned on y. The SSAs are given by

where drop has no effect on contains. Hence, for ground action α = drop(Box , Shelf ), we have LE(α) = {contains}, and NLE(α) = {on, broken}. We can confirm that α is acyclic as follows. Obviously, the dependency graph, as shown in Fig. 1, does not contain any cycles. Furthermore, for fluent broken, grounding γ+ broken by α yields on(Box , Shelf , s) ∧ contains(Box , x, s), while γbroken is simply FALSE, so both are in good form wrt on. Moreover, for fluent on, the SSA only mentions fluents from LE(α). Now let DS0 be

That is to say, Box contains Vase, Box is on Shelf , and every broken object is not contained in anything. Applying Prop. 1 to (DS0 ∪ Dss) ↑ S0, we obtain (let P, P ′ be the corresponding lifting predicates for on and broken):

Forgetting P ′ in T0 by Theorem 1 yields a sentence

By Prop. 2 and Lemma 1, it can be rewritten to be semidefinitional wrt P. Let Re(T1) be the result of rewriting T1. Now, deleting all sentences with P ′ in T0∪Re(T1), forgetting P , and replacing S0 by Sα, we have (with simplifications)



That is, Box still contains Vase, yet Box and all things contained in it are no longer on Shelf . Furthermore, all things contained in Box are broken, and all broken objects are either contained in Box , or were among the previously broken objects not contained in anything.

We note that relaxing DS0 from separable semi-definitional to semi-definitional would cause troubles. In the above example, suppose another binary fluent F(x, y) is affected globally by the action α = drop(Box , Shelf ). Let γ+ F (α, x, y, s) be on(Box, Shelf ) and γF (α, x, y, s) be FALSE. Consider DS0 = {F(x, y, S0) ⊃ on(x, y, S0)}, which is semidefinitional wrt F and on. The formula of Eq. (4b) obtained by forgetting the lifting predicate of F in the grounded theory amounts to ¬on(Box, Shelf , S0) ∧ F(x, y, Sα) ⊃ on(x, y, S0), which is no longer in good form wrt on.

For a similar reason, our approach cannot handle nonacyclic actions such as the action inc of incrementing a counter: The SSA C(x, do(a, s)) ≡ a = inc ∧ C(x - 1, s) ∨ C(x, s) would yield a self-loop C → C in the dependency graph.

Finally, requiring γ+ F (also γF ) to be in good form wrt at most one fluent in NLE(α) means the dependent fluents appear essentially as literals. This seems to be inevitable as forgetting the lifting predicate of F generates formulas involving both γ+ F and its negation (cf. Eq. (3c) and Eq. (4b)). It is desirable but also challenging to extend the result beyond formulas in good form. We leave it for future exploration.

4 Computability Results

So far, we have discussed progression in terms of FOdefinability, but did not pay attention to computability. Interestingly, LL09 showed that for local-effect actions and normal actions, the progression of so-called proper+ KBs [Lakemeyer and Levesque, 2002] is not just FO-definable, but also efficiently computable (polynomial in the size of KB) under reasonable assumptions. Here, we show that the progression of such KBs against acyclic actions is efficient as well, under similar but stronger assumptions.

Let e range over ewffs, i.e., quantifier-free formulas whose only predicate is equality. We let ∀ϕ denote the universal closure of ϕ.

Definition 10. 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.

The class of proper+ KBs is very expressive. Similar to how a standard relational database corresponds to a maximally consistent and finite set of ground literals, in the sense that every atom is known to be true iff stored in the database (and known to be false iff derivable by negation as failure), a proper+ KB corresponds to a consistent but infinite set of ground clauses, not necessarily maximal. Besides, it is shown that for certain types of queries, query evaluation against proper+ KB is efficient and can be computed in polynomial time [Liu and Levesque, 2005].

Theorem 4 ([Liu and Lakemeyer, 2009]). 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 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 Σ.

This is because every sentence in Σ can be transformed to a certain normal form wrt P(⃗c), i.e., a formula of the form ϕ1 = ∀(e1 ⊃ d1 ∨ P(⃗t)) or ϕ2 = ∀(e2 ⊃ d2 ∨ ¬P(⃗t)) where either ⃗t = ⃗c or e1 ∧ ⃗t = ⃗c (likewise for e2) is unsatisfiable. Moreover, this procedure takes O(n + 2wm) time [Liu and Lakemeyer, 2009]. In addition, forgetting P(⃗c) in the transformed proper+ KB amounts to computing all the ∀- resolvents for any two input clauses: for ϕ1 and ϕ2 as above one obtains ∀(e1∧e2 ⊃ d1∨d2), yielding a KB that is again in proper+ form. Hence the overall complexity is O(n+4wm2 ).

In the same spirit, they showed:

Theorem 5 ([Liu and Lakemeyer, 2009]). Let Σ be a proper+ KB which is semi-definitional 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.

In the above result, assuming w = O(1) and m2 = n, both forms of forgetting can be computed in O(n) time, i.e. efficiently. Hence, LL09 had the following as a theorem. An SSA is said to be 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.

Theorem 6 ([Liu and Lakemeyer, 2009]). Suppose that Dss is essentially quantifier-free, α 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.

This is by the fact that if Dss is essentially quantifier-free, then Dss[α, S0] is definable as a proper+ KB. Thereafter, one can use Theorem 5 to efficiently forget non-local-effect fluents and Theorem 4 to efficiently forget local-effect fluents via forgetting the characteristic set.

An implicit assumption of the above result is that after forgetting a non-local-effect fluent, the number of sentences involving other non-local-effect fluents in the resulting KB does not increase so that the process can be iterated to forget other non-local-effect fluents. This is indeed the case for normal actions where non-local-effect fluents only depend on localeffect ones. The situation differs for acyclic actions. For instance, in Example 2 forgetting the lifting predicate P ′ of broken will generate a formula that involves the lifting predicate P for on, i.e., T1.

Lemma 2. If ϕ(⃗x) is in good form wrt a predicate P and quantifier-free, then ϕ(⃗x) can be transformed into a set of ∀- clauses that is semi-definitional wrt P.

Proof. ∀⃗x(ψ(⃗x) ∨ P(⃗t)) can equivalently be rewritten as ∀⃗x∀⃗y. ⃗y = ⃗t ⊃ (ψ(⃗x) ∨ P(⃗y)), which has the right form if w.l.o.g. ψ is in clausal form (and quantifier-free by assumption). Similar for ∀⃗x(ψ′ (⃗x) ∨ ¬P(⃗t)) and ∀⃗xψ′′ (⃗x).

The lemma implies that although new formulas might be generated by forgetting a non-local-effect fluent for an acyclic action, the new formulas can be rewritten as a proper+ KB that is semi-definitional wrt the non-local-effect fluent it might depend on. This is crucial for the progression to iteratively forget multiple fluents.

Besides, the number of generated formulas that involve a non-local-effect fluent is linear in the size of sentences that involve the forgotten fluent (the generated sentences in Eq. (4b) and Eq. (4c) need to consider all the sufficient and necessary conditions). In addition, these formulas (conditions) will accumulate with the increase of the depth of a non-local-effect fluent in the graph. Namely, forgetting a non-local-effect fluent P with maximum depth in the dependency graph takes time O(l2 ) where l is the size of all sentences in the initial KB that involve fluents that have a path to P, including P itself. As a special case, for normal actions, we have l = m, where m is the size of sentences in the KB that involve P. Therefore, assuming l2 = n where n is the size of KB, we have:

Theorem 7. Suppose that Dss is essentially quantifier-free, α is an acyclic action, and DS0 is a proper+ KB which is seperably semi-definitional wrt NLE(α). Then the progression of DS0 wrt α is definable as a proper+ KB and can be efficiently computed.

Example 3. In Example 2, Dss is essentially quantifier-free. Moreover, consider the ground action α = drop(Box , Shelf ) and DS0 as follows:

Clearly, DS0 is a proper+ KB and is semi-definitional wrt NLE(α) (it is equivalent to the initial theory before).

Now, applying Prop. 1 to D0 ∪ Dss[α, S0] ↑ S0, we obtain the following set of ∀-clauses (marked as T ′0 ):

Forgetting P ′ in T ′0 by computing all ∀-resolvents yields the following set (marked as T ′1 )

It is easy to check that T ′1 is logically equivalent to T1 from Example 2. By introducing new variables and renaming those in T ′1 , we rewrite the second ∀-clause as x = Box ∧ y = Shelf ⊃ (P (x, y) ∨ ¬broken(x′ , Sα) ∨ contains(y′ , x′ , S0)) so that T ′1 is semi-definitional wrt P. Similarly, all sentences in T ′0 mentioning P (Box , Shelf ) can be rewritten in this way.

Now, deleting all sentences in T ′0 ∪T ′1 that mention P ′ and forgetting P, we obtain the following proper+ KB, which is equivalent to the progression result from before.



contains(Box , Vase, Sα), ¬on(Box , Shelf , Sα) ¬contains(Box , x, Sα) ∨ ¬on(x, Shelf , Sα), ¬contains (Box , x, Sα) ∨ broken(x, Sα), ¬broken(x, Sα) ∨ contains (Box , x, Sα) ∨contains (y, x, Sα) 

5 RelatedWork

In their seminal work, Lin and Reiter [1997] provided a general account of progression, extending earlier concepts such as the update of a database by means of STRIPS operators, or Pednault's [1987; 1989] ADL formalism, where databases had to be logically complete theories. There, Lin and Reiter also showed that progression is always second-order definable and that theories exist whose progression is not representable by a finite first-order theory, and they conjecture that first-order logic is generally insufficient to capture progression, even when allowing for infinite theories. This conjecture was later proved to be true in [Vassos and Levesque, 2008], where it is shown that an infinite first-order theory is generally too weak to capture all entailments of a progressed theory. Since then, efforts have been made to identify fragments where progression is first-order definable.

Lin and Reiter [1997] showed that if the KB is relatively complete, i.e. for every sentence ϕ uniform in S0, KB entails either ϕ or its negation, or, if the basic action theory is context-free, i.e. actions' effects are independent of situations, progression is FO definable in case the KB is separably semi-definitional wrt all fluents (although they did not use this terminology). Essentially, context-free actions are special cases of acyclic actions where the effect conditions γ+ F and γF do not contain fluents at all. Later, [Vassos et al., 2008] proved that progression through local-effect actions is FO definable, yet no explicit form was provided until [Liu and Lakemeyer, 2009]. In [Liu and Lakemeyer, 2009], normal actions are examined, extending the concept of localeffect actions. However, as described in this paper, their result was limited as to how non-local-effect fluents might depend on one another, a limitation we overcome with the notion of acyclic theories. [Liu and Lakemeyer, 2009] also showed that if the KB is additionally in a certain form called proper+, progression can be carried out efficiently. To capture domains that involve actions that may not be local-effect or normal, [Vassos et al., 2009] studied range-restricted action theories, i.e., theories where action effects are "bounded" in a certain sense. One appealing aspect of such action theories compared to our acyclic ones is that they allow fluents to depend on themselves, yet additional constraints have to be imposed on the action theories and initial KB (different from our notion of separably semi-definitional) to ensure a firstorder progression. The above results on local-effect, normal actions and range-restricted action theories were extended to cover functions in [Belle and Lakemeyer, 2011]. More recently, [De Giacomo et al., 2016] showed that progression is FO definable for bounded situation calculus action theories, i.e., action theories where the number of fluent instances affected by actions is bounded by a given constant.

Since its inception by Lin and Reiter [1997], progression has seen many applications and implications. [Lakemeyer and Levesque, 2009] consider only knowing a KB and show that progressing it wrt an action and sensing result amounts to only knowing another KB. This result was extended to probabilistic knowledge bases for noisy actions and sensing in [Liu and Feng, 2023]. See also [Belle and Levesque, 2014; Belle and Levesque, 2020] for the progression of a probabilistic knowledge base in the classical Situation Calculus. Other works that involve progression include [Fang et al., 2019] for multi-agent modal logic, [Schwering et al., 2015; Claßen and Delgrande, 2022] for belief revision, and [Claßen, 2013; Liu et al., 2023] for planning and verification in GOLOG. Notably, [Zarrieß and Claßen, 2016] introduced a concept of acyclic action theories that ours is inspired by, but that differs in its formal definition. 2 There, they were used to show that the verification of temporal properties for nonterminating GOLOG programs is decidable, under additional restrictions. Yet, their result is based on regression, and it was open whether (though plausible that) this implies a first-order result on progression. The result of acyclic actions provided in this paper contributes to completing the picture.

6 Conclusion

In this work, we extend the first-order progression of localeffect and normal actions by Liu and Lakemeyer [2009] and show that for acyclic actions that strictly subsume normal actions, progression is still first-order definable. Furthermore, we show that, for proper+ KBs, under similar but more stringent assumptions than made by Liu and Lakemeyer, progression is efficient as well.

For future work, a possible direction is to explore whether weaker restrictions than being in good form can be applied. Besides, a well-known algorithm for second-order quantifier elimination [Gabbay et al., 2008] is the DLS algorithm [Doherty et al., 1997], which is proven to terminate if the dependency of SO variables is subject to certain acyclicity properties [Conradie, 2006]. It would be interesting to investigate how exactly the acyclicity there is connected to our notion of acyclicity of fluents for acyclic actions.

2 [Zarrieß and Claßen, 2016] subdivides the formulas comprising γ+ F and γF into an effect descriptor and context condition. For the dependency graph, only effect descriptors are considered.

Acknowledgments

Daxin is funded by a Royal Society University Research Fellowship.