On the Size Complexity and Decidability of First-Order Progression

1 Introduction

Our motivation is derived from the aim of enabling intelligent agents to act in real-world scenarios, typically involving incomplete information about the state of the world and unbounded domains of objects. For this purpose, we use the framework of Situation Calculus [McCarthy and Hayes, 1969; Reiter, 2001], a widely studied first-order (FO) formalism for reasoning about action and change. A central problem for various reasoning tasks such as planning, verification, and synthesis, is that of projection, i.e., to determine if a query formula ϕ will hold after the execution of an action α, given a theory D consisting of a knowledge base (KB) describing the current state of affairs and axioms encoding the effects of actions. The two most common approaches are those of regressing ϕ through α and then testing the result against the original KB, and that of progressing the KB through α and then testing the original ϕ against this updated KB. Arguably, regression is less suited for practical applications because it needs to be performed for every query formula anew, while it is sufficient to determine a progression once for each action.

∗An extended version of this paper with proofs is available at arXiv:2605.12691.

†Corresponding Author.

We thus focus our attention on progression in this paper. Unfortunately, there is a strong negative result due to Lin and Reiter [1997], which says that representing the progression of an FO theory requires second-order (SO) logic in general. Identifying FO special cases, by restricting the KB or action effects, has therefore long been a central topic in reasoning about actions and change. Three increasingly expressive 1 such classes are the local-effect, normal [Liu and Lakemeyer, 2009], and acyclic [Liu and Claßen, 2024] ones, all of which were shown to be effectively FO progressable.

However, for practical feasibility, at least two additional aspects are crucial that we address in this paper. First, a formal analysis of the size complexity of such progressions has been missing. After formal preliminaries in Sec. 2, we show in Sec. 3 that under certain assumptions, the FO progression for the aforementioned classes grows only polynomially, or even linearly. Besides, we want to guarantee that queries can be effectively evaluated against the progression result, for instance by resorting to decidable fragments of first-order logic (FOL) such as the two-variable fragment FO2 [Gr¨adel et al., 1997] or universal theories with constants UTC [Arenas et al., 2018]. We hence show these fragments to be closed under progression in case of FO2 (Sec. 4) and UTC (Sec. 5). We discuss related work and conclude in Sec. 6.

2 Preliminaries

We assume familiarity with FOL including equality, here denoted by L. We will use "dot" notation to indicate that the quantifier preceding the dot has maximum scope, e.g., ∀x.ϕ(x) ⊃ ψ(x) stands for ∀x(ϕ(x) ⊃ ψ(x)). We omit leading universal quantifiers and assume free variables are implicitly ∀-quantified, e.g., we identify ϕ(x) with ∀x.ϕ(x). We use ψ ⇔ ψ to mean ϕ and ψ are logically equivalent. We denote by ϕ(µ/µ′ ) the formula obtained by simultaneously substituting every occurrence of expression (term or formula) µ in ϕ with µ′ . Let L2 denote the SO extension of L.

2.1 Situation Calculus

The Situation Calculus [Reiter, 2001] Lsc is a three-sorted language with some SO features suitable for describing dynamic worlds. The sorts are used to distinguish action, situation, and object. Lsc uses a distinct constant S0 to denote the initial situation; a binary function do(a, s) to generate the successor situation of situation s from doing action a; a binary relation Poss(a, s) to express action a being executable in situation s. We use a and s for variables of sort action and situation, respectively. Given a ground action α, we use Sα to refer to the situation do(α, S0). Fluents are predicates whose last argument is a situation term; we omit function fluents for simplicity. A (possibly SO) formula ϕ is uniform in a situation term s if ϕ mentions no situation terms except s, quantifies no situation variables, and mentions no Poss.

1 The inclusion is not exact, as we discuss in Sec. 3.

Definition 1 (Basic Action Theory). A basic action theory (BAT) in Lsc is a set of axioms

1. Σind is a set of domain-independent axioms [Levesque et al., 1998] 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

F , the conditions under which action a causes F to become true and false, respectively, have to be uniform in s and satisfy D |= ¬(γ+ F ∧ γF );

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.

2.2 Progression

A progression should retain all proper information, i.e., logical entailment in terms of the future of the initial KB. Lin and Reiter [1997] provide a model-theoretical definition of progression and prove that progression is SO definable. Vassos and Levesque [2013] prove that any correct progression is equivalent to the SO representation of [Lin and Reiter, 1997]. Here we use the definition from [Vassos and Levesque, 2013].

Let Dss[α, S0] be the instantiation of Dss wrt α and S0, i.e. Dss[α, S0] ⇔ ∧F ∀⃗x.F (⃗x, do(α, S0)) ≡ ΦF (⃗x, α, S0), where ΦF denotes the RHS of the SSA for fluent F. Let F1, . . . Fn be the set of all fluents. For each fluent Fi, we introduce a new predicate symbol Pi. Let ϕ ↑ S0 be 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.

Definition 2. Let D be a basic action theory, α an executable ground action (under Dap), and DSα a set of (FO or SO) sentences uniform in Sα. We say that DSα is a progression of DS0 wrt α, D iff Duna ∪ DSα ⇔ Duna ∧

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

Def. 2 is correct in the sense that for any ϕ uniform in Sα, if DSα is a progression of DS0 wrt α, D, then D |= ϕ iff (DDS0 ) ∪ DSα |= ϕ [Vassos and Levesque, 2013, Thm. 1].

2.3 Forgetting

There are two approaches to identifying fragments of the Situation Calculus where progression is FO definable: one that restricts the structure of the initial theory, and one that restricts action effects. We focus on the latter in this paper, in particular, we consider local-effect action theories (BATLE), normal action theories (BAT-NR), and acyclic action theories (BAT-AC). The next sections give definitions for these classes, presents the associated progression methods, and provides size complexity results as new contribution.

The progression of a theory through an action can be interpreted in terms of forgetting all information about the original state of the world, and only keeping information relevant to the new state. 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). For a sentence ϕ and ground atom P(⃗t), let ϕ[P(⃗t)] be the formula obtained by replacing every occurrence of the form P (⃗t′ ) in ϕ with [⃗t = ⃗t′ ∧P (⃗t)]∨[⃗t ̸= ⃗t′ ∧P (⃗t′ )]. Clearly, ϕ ⇔ ϕ[P(⃗t)]. Let ϕP(⃗t) + and ϕP(⃗t) - be formulas obtained by replacing P(⃗t) in ϕ[P(⃗t)] with TRUE and FALSE, respectively.

Theorem 3 ([Lin and Reiter, 1994]). Let P(⃗t) be a ground atom, P a predicate symbol, and ϕ a sentence. Then

• forget(ϕ, P(⃗t)) ⇔ϕP(⃗t) + ∨ ϕP(⃗t) - ;
• forget(ϕ, P) ⇔ ∃R.ϕ(P/R), where R is a SO variable.

Consequently, progression in Eq. (1) amounts to adding the effects of the action (Dss[α, S0]) and forgetting the truth of fluents at situation S0 (∃-quantified from the outside). Thus, progression is FO definable in cases where the SO quantifiers in (1) can be eliminated.

W.l.o.g., we assume γ± F (⃗x, a, s) in SSAs are disjunctions of formulas of the form (one for each action symbol A)

where A(⃗v) is an action term, ⃗v may contain some variables from ⃗x, and the remaining variables are ⃗z; ϕ±A (⃗x, ⃗z, s) is a formula uniform in s with no action terms, and where all free variables symbols are among ⃗x, ⃗z, and s. Under this assumption and Duna, for every ground action α = A(⃗t),

Henceforth, whenever we refer to γ± F (⃗x, α, S0), we mean the RHS of Eq. (2) and this applies to Dss[α, S0] as well.

3 Size Complexity of Progression

Previous work on the FO progression of acyclic action theories [Liu and Claßen, 2024] identified some complexity results in terms of computation time. However, the resulting theory's size is equally crucial, since it directly affects the computational costs of checking queries against the theory. Here, we identify upper bounds for the size of FO progressions for BAT-LE, BAT-NR and BAT-AC theories.

Formally, the size |ϕ| of a formula ϕ is the number of atoms (including equalities), boolean connectives from {∧, ∨, ¬}, and quantifiers from {∃, ∀} it contains. As mentioned, a formula with free variables is understood as its universal closure. Where possible, leading universal quantifiers are omitted, and do not count towards the size. Also, as usual, we identify finite theories with the conjunction of formulas they contain. To avoid confusion, when we talk about the size of such a finite theory, we always mean the size of the formula it presents, and not the number of formulas in the set.

The results in this section will present bounds for the size of the progression, which is understood as the set of sentences DSα that replaces DS0 in the BAT to reflect the state of the world in the new situation after executing ground action α. In particular (cf. Def. 2), the axioms encoding unique names for actions, Duna, are not considered part of the progression, but may be used during the construction of a progression for simplification purposes. We further assume that the vocabulary of action and fluent symbols is fixed and finite.

3.1 BAT-LE

The idea behind local-effect action theories [Liu and Lakemeyer, 2009] is to impose constraints on SSAs such that any ground action only affects finitely many objects, namely those explicitly mentioned in the action's arguments. In consequence, only finitely many fluent instances are affected.

Formally, a ground action α = A(⃗t) is said to have local effects on a fluent F if γ± F (⃗x, α, S0) in Eq. (2) is of the form ∃⃗z.[⃗t = ⃗v ∧ ϕ±A (⃗z, S0)]. We call a BAT a BAT-LE (wrt α) if α is local-effect to all fluents. For such a BAT, Duna implies γ± F (⃗x, α, S0) ≡ ∨i (⃗x = ⃗ti ∧ ϕ±A (⃗x, S0)) (as all possible occurrences of ⃗x on the RHS of Eq. (2) are among ⃗v). Hence, there are only finitely many affected fluent instances, i.e., the characteristic set Ω(s) given by

where ΦF (⃗t, α, S0) is the right-hand side of the SSA for F. Liu and Lakemeyer [2009] observe that for BAT-LE, forgetting predicates in the progression as in Eq. (1) can be done via forgetting the ground atoms in Ω: If θ is a consistent, finite set of ground literals, let ϕ[θ] denote the result of replacing every occurrence of an atom P(⃗t) in ϕ by the formula

where for j = 1, . . . , k, θ specifies truth value vj for P(⃗tj). Theorem 3.6 of [Liu and Lakemeyer, 2009] states that the following is then a progression of DS0 wrt α, D:

Here, M(Ω(S0)) denotes the set of all maximal consistent sets of literals over the atoms in Ω(S0). The big disjunction in Eq. (4) essentially amounts to forget(DS0 ∪Dss[Ω],ΩS0 ) (which means iteratively forgetting atoms in Ω(S0)). The claim in the following theorem was already stated in [Liu and Lakemeyer, 2009], however, without a proof.

Theorem 4. If D is BAT-LE wrt ground action α, then its progression can be represented by a FO theory of size O(2c (n +m)), where c is the size of the characteristic set, n is the size of DS0 , and m is the size of Dss.

Proof. The size of DS0 is n by assumption, and the size of Dss[Ω] is bounded by cm + c - 1, since there are c many formulas in Dss[Ω], each of size less or equal to m, with (c1) conjunction symbols between them. If ϕ denotes DS0 ∪ Dss[Ω], we hence have |ϕ| ≤ n + cm + c.

Observe that for any θ ∈ M(Ω(S0)), the number of elements in θ is the same as the number of elements in Ω, i.e., c. In particular, in (3), k ≤ c. If a denotes the maximal arity of any predicate P in ϕ, ⃗t = ⃗tj abbreviates a formula of size less than 2a, and so the size of the formula in (3) is bounded by 4ca+4c+3. Therefore, for any ϕ, |ϕ[θ]| ≤ (4ca+4c+3)|ϕ|.

Finally, observe that the step (S0/Sα) substitutes one constant by another, and hence does not change the size of the formula. Also, there are 2c many θ's in M(Ω(S0)). As argued above, the size of Duna can be ignored. In summary, we can estimate the size of the progression to be no more than 2c · (n+ cm+ c) · (4ca + 4c + 3). Since a is constant under the assumption of a fixed vocabulary, we get that the size of the progression is in O(2c (n +m)).

We remark that c can be bounded by a constant. Note that the elements of Ω[S0] are of the form F(⃗t, S0), where F is a local-effect fluent, and the ⃗t have to be chosen from the arguments of ground action α. Therefore, if l is the number of local-effect fluents, b is the arity of α, and a is again the maximal arity among predicates, c ≤ l · ba , where all of l, a, and b are constant under the assumption of a fixed vocabulary. It can hence also be argued that the size of the progression of a BAT-LE is linear in the size of the original theory.

3.2 BAT-NR

To facilitate global effects, BAT-NR relaxes the restriction on SSAs but imposes additional assumptions on DS0 so that one can use a variant Ackermann's Lemma [Ackermann, 1935] to eliminate SO quantifiers. Formally, 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 be the set formulas ψ(⃗x) such that ψ(⃗x) ⊃ P(⃗x) is in T, and SNCP be the set of formulas ϕ(⃗x) with P(⃗x) ⊃ ϕ(⃗x) in T . Then the following holds:

Theorem 5 ([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 ′ ∧ ∧ψ∈WSCP ,ϕ∈SNCP ∀⃗x.ψ(⃗x) ⊃ ϕ(⃗x).

Proposition 6. In any model of D, the SSA for F instantiated by ground action α, DF ss [α, S0], is equivalent to:

We say a formula ϕ is semi-definitional wrt a fluent F if ϕ ↑ S0 is semi-definitional wrt F's lifting predicate. The proposition suggests that DF ss [α, S0] for every fluent F is semi-definitional wrt F. Hence, if DS0 is also semidefinitional wrt fluents, one can use Thm. 5 to forget their lifting predicates in Eq. (1), which is the idea behind normal actions and their progression. For an action α, we distinguish local-effect fluents LE(α) on the one hand (whose SSAs are as in BAT-LE), and non-local effect fluents NLE(α) on the other hand. Normal actions then require that for all F ∈ NLE(α), fluents occurring in γ± F can only be in LE(α). We call a BAT D a BAT-NR (wrt action α) if α is normal and DS0 is semi-definitional wrt fluents in NLE(α). For such a BAT, one can forget lifting predicates of fluents in NLE(α) by Thm. 5 and thereafter fluents in LE(α) as in Eq. (4).

Theorem 7. If D is BAT-NR wrt ground action α, the result of forgetting the lifting predicates for all fluents in NLE(α) in (DS0 ∪ Dss[α, S0]) ↑ S0 can be represented by a FO theory whose size is in O((n+m)2 ), where n is the size of DS0 , and m is the size of Dss.

Proof. First, note that we can ignore the lifting operator ↑ S0 here, since it only replaces atoms by other atoms, and thus does not affect the size of a formula. Now, assume that for fluents F ∈ NLE(α), axioms in Dss[α, S0] are represented according to Prop. 6. Note that (5a) and (5b) are semi-definitional wrt F(⃗x, S0), and (5c) and (5d) do not mention F(⃗x, S0). Theorem 5 is hence applicable to DS0 ∪ Dss[α, S0]. Intuitively, the set of semi-definitional formulas in DS0 ∪ Dss[α, S0] can be represented as a directed graph, where any formula ψ(⃗x) ⊃ ϕ(⃗x) corresponds to an edge from ψ(⃗x) to ϕ(⃗x). Forgetting the lifting predicate for a fluent F ∈ NLE(α) then amounts to eliminating the node for F(⃗x, S0), "bypassing" all involved edges, i.e., every pair of ingoing edge ψ(⃗x) ⊃ F(⃗x, S0) and outgoing edge F(⃗x, S0) ⊃ ϕ(⃗x) is replaced by a new edge ψ(⃗x) ⊃ ϕ(⃗x). This elimination operation is performed iteratively for all F ∈ NLE(α) (in any order), leaving only nodes that correspond to conditions that do not mention any of the non-local-effect fluents. In the worst case, the resulting graph is total, i.e., every condition is connected to every other condition through an edge. Since the size of all conditions together is bounded by n +m, the size of the theory representing all combinations of implications between them is in O((n+m)2 ). Moreover, the size of the original formulas in DS0 ∪Dss[α, S0] that do not mention any of the NLE fluents (including (5c) and (5d)) is bounded by n+m as well. All in all, the size of the resulting theory is thus in O((n+m)2 ).

According to [Liu and Lakemeyer, 2009], the progression of a BAT-NR through an action α is obtained by first forgetting the (lifting predicates) of the fluents in NLE(α), and afterwards forgetting the remaining atoms over the fluents in LE(α). We can estimate the size of the resulting theory by combining the results from Theorems 4 and 7, giving:

Corollary 8. If D is BAT-NR wrt ground action α, then its progression can be represented by a FO theory of size O(2c (n +m)2 ), where c is the size of the characteristic set, n is the size of DS0 , and m is the size of Dss.

3.3 BAT-AC

While normal action theories allow for non-local effects of a certain form, they include the requirement that for BATNR, the effect conditions γ± F for a fluent F may only mention local-effect fluents. This assumption ensures that forgetting the lifting predicate for F will not generate formulas that mention the lifting predicate of another NLE fluent F ′ , which might not have the right (semi-definitional) form to proceed with forgetting F ′ in the same manner. However, this excludes domains where actions' effects for a NLE fluent might depend on the state of another NLE fluent. BAT-AC, the class of acyclic action theories [Liu and Claßen, 2024] overcomes this restriction by allowing NLE fluents to depend on one another, as long the dependencies do not form any cycles. Here, additional restrictions on the form of γ± F guarantee that the lifting predicates for NLE fluents can be forgotten in a recursive fashion when following the order of dependencies among fluents. Formally, a formula ϕ(⃗x) is said to be in good form wrt a predicate P if it is of the form

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

Proposition 9 ([Liu and Claßen, 2024]). If ϕ(⃗x) is in good form wrt P, then

1. ϕ(⃗x) can be rewritten to be semi-definitional wrt P;

2. ¬ϕ(⃗x) can be rewritten to be in good form wrt P .

Now, given SSAs Dss and a ground action α, the dependency graph G for Dss wrt α is a directed graph whose vertices are the set of fluents and there is an edge F → F ′ for two fluents F, F ′ iff F ∈ NLE(α) and F ′ appears in γ± F . A ground action α is acyclic (or has acyclic effects) if 1) its dependency graph G is acyclic, i.e., a DAG; and 2) for each fluent F , there are at most two fluents F ′ , F ′′ in NLE(α) such that F → F ′ and F → F ′′ , where γ+ F and γF are in good formwrt F ′ and F ′′ , respectively.

We call a BAT a BAT-AC (wrt α), if α is acyclic and DS0 is separably semi-definitional wrt NLE(α), that is, each sentence in DS0 mentions at most one fluent F in NLE(α) and is semi-definitional wrt F. [Liu and Claßen, 2024] showed that if a BAT D is a BAT-AC, the progression of DS0 wrt α, D is FO definable. This is because for any F, F ′ ∈ NLE(α), even if forgetting the lifting predicate of F will possibly generate new formulas that mention F ′ , the assumption of γ± F being in good form wrt F ′ ensures that the new formulas can be rewritten to be semi-definitional wrt F ′ again. Hence, one can recursively forget lifting predicates for F ∈ NLE(α) (following the order of the DAG) and later forget lifting predicates of F ∈ LE(α) as in Eq. (4). For analyzing the size of the resulting theory, we need the following:

Definition 10. If ϕ(⃗x) is in good form wrt P, i.e., ϕ(⃗x) := (ψ(⃗x)∨P(⃗t))∧(ψ′ (⃗x)∨¬P(⃗t))∧ψ′′ (⃗x), we define |ϕ|P = max{|ψ|, |ψ′ |, |ψ′′ |} as the condition size of ϕ wrt P .

As we will see, the size of conditions within good-form formulas will be the determining factor for the size complexity of a progression for a BAT-AC. Furthermore, we assume

This is without loss of generality: If DS0 contains multiple semi-definitional formulas for F, let NWSF be the negation of the weakest sufficient condition, and SNCF the strongest necessary condition. Observe that with the implicit negation in NWS, ∆F is indeed in semi-definitional form, and such formulas can be assumed to be of good form (6). Also, this assumption has no impact on size or condition size:

Proposition 11. If ϕ1(⃗x), ϕ2(⃗x), . . . , ϕn(⃗x) are all semidefinitional wrt predicate P , then ϕ1(⃗x)∧ϕ2(⃗x)∧· · ·∧ϕn(⃗x) can be rewritten to a single equivalent formula φ(⃗x) such that |φ(⃗x)| ≤ | ∧i ϕi(⃗x)| and |φ(⃗x)|P ≤ | ∧i ϕi(⃗x)|P .

Next, we consider formulas in good form and how rewriting them as in Prop. 9 affects the size of the result:

Proposition 12. If ϕ(⃗x) is in good form wrt P, then

1. ϕ(⃗x) can be rewritten to φ(⃗y) that is semi-definitional wrt P(⃗y), moreover, if a = max{|⃗x|, |⃗y|}, then |φ(⃗y)| ≤ |ϕ(⃗x)| + 7a + 2 and |φ(⃗y)|P ≤ |ϕ(⃗x)|P + 3a + 1;
2. ¬ϕ(⃗x) can be rewritten to φ(⃗x) that is in good form wrt P with |φ(⃗x)| ≤ 3|ϕ(⃗x)| and |φ(⃗x)|P ≤ 3|ϕ(⃗x)|P + 2;
3. if ψ(⃗x) mentions noP, then ϕ(⃗x)∨ψ(⃗x) can be rewritten to a formula φ(⃗x) in good form wrt P, where |φ(⃗x)| = |ϕ(⃗x)|+3|ψ(⃗x)|+3 and |φ(⃗x)|P = |ϕ(⃗x)|P +|ψ(⃗x)|+1.

Then we have:

Theorem 13. If D is BAT-AC wrt ground action α, the result of forgetting the lifting predicates for all fluents in NLE(α) in (DS0 ∪ Dss[α, S0]) ↑ S0 can be represented by a FO theory whose size is in O(2d (n +m)), where d is the depth of the dependency graph, n the size of DS0 , and m the size of Dss.

Proof. The proof for Theorem 3 in [Liu and Claßen, 2024] makes an inductive argument that one can forget fluents F ∈ NLE(α) iteratively while maintaining the required form, as long as one forgets all predecessors of F in the dependency graph before forgetting F itself. By Prop. 6 and Thm. 5, forgetting any such F amounts to replacing the corresponding ∆F by the following (parameters of γ± F are omitted):

By definition, there are at most two other NLE fluents F1, F2 with F → F1 and F → F2, where F1 only occurs in γ+ F , and F2 only in γF . (7b) and (7d) will subsequently be incorporated into the new axiom ∆F1 , and (7c) and (7e) into the new axiom ∆F2 . If wF is the condition size of the updated ∆F and k the maximal size of an SSA for any NLE fluent, then by Prop. 12, upper bounds for the condition sizes of formulas (7b)-(7e) after rewriting them to be in good form wrt. F1, F2 are as stated above in parentheses. If w is an upper bound for the condition size of any original ∆F axiom, the condition size for the updated ∆F ′ is bounded according to

The sum of the sizes of (7a)-(7e) over all NLE fluents F gives an upper bound for the size of the progression. Observe that the total size of γ± F , F(⃗x, Sα) atoms, and boolean connectives is less than |DF ss [α, S0]| as in Prop. 6, i.e., less than m summed over all NLE fluents. This leaves two occurrences of NWSF (⃗x) and two of SNCF (⃗x), each of size ≤ wF , summing up to S = 4 ∑F∈NLE(α) wF . To determine the sum of all wF , we use the intuition that the linear recurrence in (8) can be unrolled along all source-to-node paths. Intuitively, each node F starts with a wF "weight" of w and adds wF +4k+6a+10 to each of its children. This contribution is added multiple times, namely for each path starting in F . As the out-degree of nodes is ≤ 2, the number of distinct paths starting in F is ≤ 2d+1 . If l is the number of NLE fluents, we get S ≤ 4 · 2d+1 · l · (w+4k+6a+10). Since a is a constant, l · w ∈ O(n), and l · k ∈ O(m), the claim follows.

Combining the above theorem with Theorem 4 again yields:

Corollary 14. If D is BAT-AC wrt ground action α, then its progression can be represented by a FO theory of size O(2c+d (n + m)), where c is the size of the characteristic set, d is the depth of the dependency graph, n is the size of DS0 , and m is the size of Dss.

Observe that the progression for BAT-LE and BAT-AC is linear in the size of the theory, while that for BAT-NR is quadratic. As mentioned previously, the three classes roughly form a hierarchy of increasing expressiveness, but not exactly. This is because BAT-NR allow "mixed" semi-definitional axioms of the form F (⃗x, S0) ⊃ G(⃗x, S0), where both F and G are NLE fluents, whereas BAT-AC requires a strict separation so that a semi-definitional axiom for F does not mention any NLE fluent G, and vice versa. If we impose this additional restriction on BAT-NR, the resulting class will indeed be a proper subset of BAT-AC, consisting of action theories whose dependency graph has a depth of at most one, and where every edge F → G is between an NLE fluent F and a LE fluent G. The size of the progression then is in O(2c (n+m)).

4 The Two-Variable Fragment

For practical applications like FO planning, it is not enough to have an FO progression, but the progressed KB has to admit effective query evaluation. This necessitates a decidable progressed theory. A class of theory T is called decidable if for any T, ϕ ∈ T , it is decidable to check if T |= ϕ. One popular decidable class of FO theories is the two-variable fragment with equality, called FO2 [Gr¨adel et al., 1997]. It consists of all formulas with at most 2 variable symbols, which we denote as x and y by convention. By ⃗x we then mean a vector of variables that either consists only of x or of x and y.

Theorem 15 ([Gr¨adel et al., 1997]). FO2 has the exponential model property: there is a constant c s.t. every satisfiable FO2 -sentence ϕ has a model of cardinality at most 2c|ϕ| , where |ϕ| is the size of ϕ.

Consequently, satisfiability of FO2 is NEXPTIME-complete and entailment checking is CoNEXPTIME-complete.

Typically, FO2 does not include general function symbols. Yet, in some literature, constant symbols are allowed as they can be simulated through unary predicates whose extensions consist of exactly one element. That is to say, for any constant A, one introduces a predicate PA(x) and includes an axiom

saying that there is exactly one domain element in the extension of PA. It is easy to see that this idea can be extended to also include ground situation terms do(α, S0).

Moreover, in the following, we assume that every rigid relation symbol has arity at most two. Again, relations of higher arity can be simulated by introducing new predicate symbols, with formulas growing at most linearly in size. For details, we refer the reader to [Gr¨adel et al., 1997]. For fluent predicates, we allow for up to two object arguments in addition to the situation argument. The idea here is that the situation argument is irrelevant, as it will be instantiated by some ground situation term when evaluating queries.

Definition 16. Given a ground action α, a BAT D is an FO2 - BAT wrt α if DS0 ∪ Dss[α, S0] is a finite FO2 theory.

In what follows, we show that the progressions of FO2 - BATs wrt local-effect, normal, and acyclic actions are all within the FO2 fragment, hence decidable.

FO2 -BAT-LE To begin with, we consider FO2 -BATwhere the action α has local effects, i.e., FO2 -BAT-LE.

Theorem 17. Given a BAT D that is BAT-LE wrt ground action α, if D is also an FO2 -BAT wrt α, then the progression of D0 wrt D, α can be expressed in FO2 .

It is not hard to check that (DS0 ∪Dss[Ω])[θ] in Eq. (4) is in FO2 by assumption. Besides, a disjunction of FO2 theories is still in FO2 , so the progression as in Eq. (4) is in FO2 .

FO2 -BAT-NR For FO2 -BATwith normal actions, we have Theorem 18. Given a BAT D that is BAT-NR wrt ground action α, if D is an FO2 -BAT wrt α, then the progression of D0 wrt D, α can be expressed in FO2 .

For BAT-NR, forgetting NLE fluents as in Thm. 5 involves combining sufficient conditions and necessary conditions of semi-definitional formulas, which clearly does not introduce new variables. Hence, the result is still in FO2 . Besides, for LE fluents, as mentioned before, forgetting them only involves disjoining two FO2 theories, which is still in FO2 . Hence, the resulting progression is in FO2 .

FO2 -BAT-AC The situation for FO2 -BAT with acyclic actions is slightly more complicated, as we need to ensure that the generated formulas when forgetting an NLE fluent are semi-definitional wrt another NLE fluent and the rewrite has to be in FO2 . The following lemma justifies this.

Lemma 19. If ϕ(⃗x) ∈ FO2 is in good form wrt P, then

1. ϕ(⃗x) can be rewritten to a formula in FO2 that is semidefinitional wrt P ;
2. ¬ϕ(⃗x) can be rewritten to a formula in FO2 that is in good form wrt P .

The proof of Item 2 is simple, as the rewrite only involves pushing negation inward and distributing conjunctions over disjunctions, operations that preserve membership in FO2 . For Item 1, let ϕ(⃗x) = {∀⃗x(ψ(⃗x) ∨ P(⃗t)), ∀⃗x(ψ′ (⃗x) ∨ ¬P(⃗t)), ∀⃗xψ′′ (⃗x)}. By assumption, ⃗x denotes either only x or x and y. Since P is unary or binary, ⃗t has length one or two, and since functions are excluded, ⃗t can only consist of a combination of x, y, and some constants A and B. Hence, for ∀⃗x(ψ(⃗x) ∨ P(⃗t)) (likewise for the ¬P case), we have cases:

• ∀x(ψ(x)∨P(A)) ⇔ ∀x((x = A)∧∃x¬ψ(x)) ⊃ P(x).
• ∀x(ψ(x) ∨P(x)) has the right form already.
• ∀x∀y(ψ(x, y) ∨ P(A, B)) can be rewritten as ∀x∀y((x = A ∧ y = B) ∧ ∃x∃y¬ψ(x, y)) ⊃ P (x, y).
• ∀x∀y(ψ(x, y) ∨ P(x, B)) can be rewritten as ∀x∀y((y = B) ∧ ∃y¬ψ(x, y)) ⊃ P (x, y).
• ∀x∀y(ψ(x, y) ∨ P(A, y)) can be rewritten as ∀x∀y((x = A) ∧ ∃x¬ψ(x, y)) ⊃ P (x, y).
• ∀x∀y(ψ(x, y) ∨ P(x, y)) has the right form already.

Hence ∀⃗x(ψ(⃗x)∨P(⃗t)), thus ϕ(⃗x), can be expressed in FO2 .

Theorem 20. Given a BAT D that is BAT-AC wrt ground action α, if D is a FO2 -BAT wrt α, then the progression of D0 wrt D, α can be expressed in FO2 .

We remark that the results in this section are not obvious in the following sense. FO2 is a fragment that fails to have the Craig interpolation and Beth definability properties [Jung and Wolter, 2021]. Among other things, this means that while forgetting a predicate P from a FO2 theory might be possible (i.e., yields an equivalent FO theory), it can happen that the resulting theory is not expressible in FO2 . Hence, not every FO2 -BAT has a progression that is in FO2 , but for the fragments we consider here, this can be guaranteed.

5 Universal Theories with Constants

Another decidable fragment of FOL is given by universal theories with constants (UTC). In fact, it is shown that BernaysSch¨onfinkel [1928] (BS) theories are decidable, i.e., theories with sentences of the form ∃x1 . . . ∃xk∀y1 · · · ∀ymϕ, where ϕ is a quantifier-free formula (potentially with equalities) mentioning no functions except constants. Satisfiability checking of BS theories is NEXPTIME-complete. UTC theories are a special case of BS theories where all sentences are universally quantified, i.e., of the form ∀y1 · · · ∀ymϕ. For UTC theory T and query ϕ, deciding if T |= ϕ can be converted to check if the BS theory T ∪{¬ϕ} is unsatisfiable, hence the complexity is CoNEXPTIME-complete.

Definition 21. Given a ground action α, a BAT D is a UTCBAT wrt α if DS0 ∪ Dss[α, S0] is a finite UTC theory.

In what follows, we show that the progressions of UTCBATs wrt local-effect, normal, and acyclic actions are all within the UTC fragment, hence decidable.

UTC-BAT-LE First, for local effect actions, we have that

Theorem 22. Given a BAT D that is BAT-LE wrt ground action α, if D is an UTC-BAT wrt α, then the progression of D0 wrt D, α can be expressed in UTC.

Again, the key here is to show that the disjunction of UTC theories can be expressed in UTC. This is indeed the case by applying the following rule to properly rename variables ∀⃗xϕ(⃗x) ∨ ∀⃗xψ(⃗x) ⇔ ∀⃗x∀⃗y(ϕ(⃗x) ∨ ψ(⃗y)).

UTC-BAT-NR Likewise, for normal actions, we have

Theorem 23. Given a BAT D that is BAT-NR wrt ground action α, if D is an UTC-BAT wrt α, then the progression of D0 wrt D, α can be expressed in UTC.

The proof is like its counterpart in FO2 , it suffices to show that forgetting NLE fluents preserves membership in UTC. This is indeed the case as the sufficient and necessary conditions to be combined when forgetting NLE fluents, as in Thm. 5, are all quantifier-free by assumption; hence, the result is still quantifier-free, leading to a UTC FO progression.

UTC-BAT-AC Lastly, for acyclic actions, we have that Lemma 24. If ϕ(⃗x) ∈ UTC is in good form wrt P, then

1. ϕ(⃗x) can be rewritten to a formula in UTC that is semidefinitional wrt P ;
2. ¬ϕ(⃗x) can be rewritten to a formula in UTC that is in good form wrt P .

Again, Item 2 is trivial as the rewrite only involves pushing negation inward and distributing conjunctions over disjunctions, operations that preserve membership in UTC. We prove the first item. For Item 1, let ϕ(⃗x) = {∀⃗x(ψ(⃗x) ∨ P(⃗t)), ∀⃗x(ψ′ (⃗x) ∨ ¬P(⃗t)), ∀⃗xψ′′ (⃗x)}. ψ(⃗x), ψ′ (⃗x), ψ′′ (⃗x) are all quantifier-free and ⃗t can only contain variables in ⃗x by assumption. ∀⃗x(ψ(⃗x) ∨ P(⃗t)) (likewise for the ¬P case) can be rewritten as ∀⃗x∀⃗y.⃗y = ⃗t ⊃ (ψ(⃗x) ∨ P(⃗y)), which is in UTC and semi-definitional wrt P , and hence so can ϕ(x).

Theorem 25. Given a BAT D that is BAT-AC wrt ground action α, if D is an UTC-BAT wrt α, then the progression of D0 wrt D, α can be expressed in UTC.

We remark that the fact that the progression of a UTC-BAT can be expressed by another UTC theory here is not so surprising, as [Arenas et al., 2018] showed that the progression of a UTC-BAT wrt any actions can be expressed by another UTC theory. In fact, a resolution-like algorithm is proposed there to compute such a progression. Nevertheless, the progression might not be finite, and deciding if a finite progression exists is undecidable; namely, the proposed algorithm might not terminate. In this regard, our contribution here is that we show that if the actions are furthermore local-effect, normal, or acyclic, finite progressions of the respective UTCBATs actually exist (and can be computed accordingly). In addition, due to our results in Section 3, the size of such finite progressions grows only polynomially, even linearly.

6 RelatedWork and Discussion

In this paper, we studied the size complexity and decidability of FO progressions in terms of local-effect, normal, and acyclic actions. Previous contributions along similar lines include those due to Liu and Lakemeyer [2009] and due to Liu and Claßen [2024], who showed that a progression can be efficiently computed for normal and acyclic theories, respectively, under the restrictions that the instantiated SSAs are quantifier-free and that the initial theory is in so-called proper+ form. Intuitively, proper+ KBs [Lakemeyer and Levesque, 2002] correspond to consistent, potentially infinite sets of ground clauses. What makes them particularly interesting is that certain queries can be computed in polynomial time [Liu and Levesque, 2005]. De Giacomo et al. [2016] showed that progression is FO definable for Situation Calculus theories where the number of fluent instances affected by an action is bounded, in which case verification (and hence projection) is decidable. Arenas et al. [2018] investigate the feasibility and complexity of progression for UTC-based action theories (without the additional restriction of SSAs to local-effect, normal or acyclic form as done here). Eiter and Sold`a [2024] studied computational aspects of progression in the context of temporal equilibrium logic.

More broadly, related work includes that by Gu and Soutchanski [2010] who studied the complexity of regression for action theories over the two-variable fragment of FOL with counting quantifiers as well as description logics ALCO(U) and ALCQO(U). Lakemeyer and Levesque [2014] presented a variant of the modal epistemic Situation Calculus based on a model of limited belief that admits a decidable, yet incomplete form of reasoning. Calvanese et al. [2015] proved that Situation Calculus theories extended with description logic TBoxes acting as state constraints lead to undecidability of the satisfiability problem, even for the simplest kinds of description logics, and the simplest kind of action theories. When TBoxes are merely viewed as part of the initial theory rather than state constraints, Zarrieß [2018] showed that the verification problem (which subsumes the projection problem) for action formalisms based on various description logics becomes decidable, providing exact complexities. Note that while many description logics can be viewed as fragments of FO2 , related results on projection are not directly applicable to a FO2 -based Situation Calculus since translating FO2 into description logic leads to a (provably unavoidable) exponential blow-up [Lutz et al., 2001].

Possible directions for future work include exploring whether more expressive classes, or less expressive but more tractable classes, admit similar closure properties as presented here. Our results also suggest the possibility to use progression instead of regression for the purpose of decidable verification of Golog as in [Zarrieß and Claßen, 2016]. Our main motivation however is in practical applications, i.e., equipping real-world agents with the capacity to plan and act in the presence of incomplete information and unbounded domains. There is a recent trend in AI planning to work directly on FO representations [Corrˆea and De Giacomo, 2024], but merely as a way to avoid the bottleneck of grounding over the given set of objects, which is still assumed to be finite. When it comes to the full expressiveness of Situation Calculus (within decidability bounds), there is currently a lack of concrete implementations and corresponding benchmarks. We believe that our work here lays the foundations towards such planning systems that work in truly open worlds.

Acknowledgements

Daxin is funded by the National Natural Science Foundation of China (NSFC No. 62506152) and the Fundamental and Interdisciplinary Disciplines Breakthrough Plan of the Ministry of Education of China (No. JYB2025XDXM118).