On the Size Complexity and Decidability of First-Order Progression

# On the Size Complexity and Decidability of First-Order Progression1footnote 11footnote 1Extended version of identically-titled paper at IJCAI 2026.
Source: [https://arxiv.org/html/2605.12691](https://arxiv.org/html/2605.12691)
Daxin Liu222footnotemark:2 1Department of People and Technology, Roskilde University, Denmark 2State Key Laboratory for Novel Software Technology, Nanjing University, China classen@ruc\.dk, daxin\.liu@nju\.edu\.cn

###### Abstract

Progression, the task of updating a knowledge base to reflect action effects, generally requires second\-order logic\. Identifying first\-order special cases, by restricting either the knowledge base or action effects, has long been a central topic in reasoning about actions\. It is known that local\-effect, normal, and acyclic actions, three increasingly expressive classes, admit first\-order progression\. However, a systematic analysis of the size of such progressions, crucial for practical applications, has been missing\. In this paper, using the framework of Situation Calculus, we show that under reasonable assumptions, first\-order progression for these action classes grows only polynomially\. Moreover, we show that when the KB belongs to decidable fragments such as two\-variable first\-order logic or universal theories with constants, the progression remains within the same fragment, ensuring decidability and practical applicability\.

## 1Introduction

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 CalculusMcCarthy and Hayes \([1969](https://arxiv.org/html/2605.12691#bib.bib24)\); Reiter \([2001](https://arxiv.org/html/2605.12691#bib.bib23)\), 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 ofprojection, i\.e\., to determine if a query formulaϕ\\phiwill hold after the execution of an actionα\\alpha, given a theory𝒟\\mathcal\{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 ofregressingϕ\\phithroughα\\alphaand then testing the result against the original KB, and that ofprogressingthe KB throughα\\alphaand then testing the originalϕ\\phiagainst 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\.

We thus focus our attention on progression in this paper\. Unfortunately, there is a strong negative result due to Lin and ReiterLin and Reiter \([1997](https://arxiv.org/html/2605.12691#bib.bib19)\), 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 expressive222The inclusion is not exact, as we discuss in Sec\.[3](https://arxiv.org/html/2605.12691#S3)\.such classes are the local\-effect, normalLiu and Lakemeyer \([2009](https://arxiv.org/html/2605.12691#bib.bib2)\), and acyclicLiu and Claßen \([2024](https://arxiv.org/html/2605.12691#bib.bib6)\)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](https://arxiv.org/html/2605.12691#S2), we show in Sec\.[3](https://arxiv.org/html/2605.12691#S3)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 fragmentFO2\\textsc\{FO\}^\{2\}Grädelet al\.\([1997](https://arxiv.org/html/2605.12691#bib.bib20)\)or universal theories with constantsUTCArenaset al\.\([2018](https://arxiv.org/html/2605.12691#bib.bib5)\)\. We hence show these fragments to be closed under progression in case ofFO2\\textsc\{FO\}^\{2\}\(Sec\.[4](https://arxiv.org/html/2605.12691#S4)\) andUTC\(Sec\.[5](https://arxiv.org/html/2605.12691#S5)\)\. We discuss related work and conclude in Sec\.[6](https://arxiv.org/html/2605.12691#S6)\.

## 2Preliminaries

We assume familiarity with FOL including equality, here denoted byℒ\{\\cal L\}\. We will use “dot” notation to indicate that the quantifier preceding the dot has maximum scope, e\.g\.,∀x\.ϕ​\(x\)⊃ψ​\(x\)\\forall x\.\\phi\(x\)\\supset\\psi\(x\)stands for∀x​\(ϕ​\(x\)⊃ψ​\(x\)\)\\forall x\(\\phi\(x\)\\supset\\psi\(x\)\)\. We omit leading universal quantifiers and assume free variables are implicitly∀\\forall\-quantified, e\.g\., we identifyϕ​\(x\)\\phi\(x\)with∀x\.ϕ​\(x\)\\forall x\.\\phi\(x\)\. We useψ⇔ψ\\psi\\Leftrightarrow\\psito meanϕ\\phiandψ\\psiare logically equivalent\. We denote byϕ​\(μ/μ′\)\\phi\(\\mu/\\mu^\{\\prime\}\)the formula obtained by simultaneously substituting every occurrence of expression \(term or formula\)μ\\muinϕ\\phiwithμ′\\mu^\{\\prime\}\. Letℒ2\{\\cal L\}^\{2\}denote the SO extension ofℒ\{\\cal L\}\.

### 2\.1Situation Calculus

The Situation CalculusReiter \([2001](https://arxiv.org/html/2605.12691#bib.bib23)\)ℒs​c\{\\cal L\}\_\{sc\}is a three\-sorted language with some SO features suitable for describing dynamic worlds\. The sorts are used to distinguish*action*,*situation*, and*object*\.ℒs​c\{\\cal L\}\_\{sc\}uses a distinct constantS0S\_\{0\}to denote the initial situation; a binary function𝑑𝑜​\(a,s\)\\mathit\{do\}\(a,s\)to generate the successor situation of situationssfrom doing actionaa; a binary relation𝑃𝑜𝑠𝑠​\(a,s\)\\mathit\{Poss\}\(a,s\)to express actionaabeing executable in situationss\. We useaaandssfor variables of sort action and situation, respectively\. Given a ground actionα\\alpha, we useSαS\_\{\\alpha\}to refer to the situationd​o​\(α,S0\)do\(\\alpha,S\_\{0\}\)\.*Fluents*are predicates whose last argument is a situation term; we omit function fluents for simplicity\. A \(possibly SO\) formulaϕ\\phiisuniformin a situation termssifϕ\\phimentions no situation terms exceptss, quantifies no situation variables, and mentions no𝑃𝑜𝑠𝑠\\mathit\{Poss\}\.

###### Definition 1\(Basic Action Theory\)\.

A*basic action theory*\(BAT\) inℒs​c\{\\cal L\}\_\{sc\}is a set of axioms

𝒟=Σi​n​d∪𝒟a​p∪𝒟s​s∪𝒟u​n​a∪𝒟S0,where\\mathcal\{D\}=\\Sigma\_\{ind\}\\cup\\mathcal\{D\}\_\{ap\}\\cup\\mathcal\{D\}\_\{ss\}\\cup\\mathcal\{D\}\_\{una\}\\cup\\mathcal\{D\}\_\{S\_\{0\}\},\\textrm\{where\}1. 1\.Σi​n​d\\Sigma\_\{ind\}is a set of domain\-independent axiomsLevesqueet al\.\([1998](https://arxiv.org/html/2605.12691#bib.bib27)\)that ensure situations are well\-structured;
2. 2\.𝒟a​p\\mathcal\{D\}\_\{ap\}is a set of action precondition axioms;
3. 3\.𝒟s​s\\mathcal\{D\}\_\{ss\}is a set of successor state axioms \(SSAs\), one for each fluent predicateFF, of the form F​\(x→,𝑑𝑜​\(a,s\)\)≡γF\+​\(x→,a,s\)∨¬γF−​\(x→,a,s\)∧F​\(x→,s\),F\(\\vec\{x\},\\mathit\{do\}\(a,s\)\)\\equiv\\gamma^\{\+\}\_\{F\}\(\\vec\{x\},a,s\)\\vee\\neg\\gamma^\{\-\}\_\{F\}\(\\vec\{x\},a,s\)\\land F\(\\vec\{x\},s\),whereγF\+\\gamma^\{\+\}\_\{F\}andγF−\\gamma^\{\-\}\_\{F\}, the conditions under which actionaacausesFFto become true and false, respectively, have to be uniform inssand satisfy𝒟⊧¬\(γF\+∧γF−\)\\mathcal\{D\}\\models\\neg\(\\gamma^\{\+\}\_\{F\}\\land\\gamma^\{\-\}\_\{F\}\);
4. 4\.𝒟u​n​a\\mathcal\{D\}\_\{una\}is the set of unique names axioms for actions:A​\(x→\)≠A′​\(y→\)A\(\\vec\{x\}\)\\neq A^\{\\prime\}\(\\vec\{y\}\), andA​\(x→\)=A​\(y→\)⊃x→=y→A\(\\vec\{x\}\)=A\(\\vec\{y\}\)\\supset\\vec\{x\}=\\vec\{y\}, whereA,A′A,A^\{\\prime\}are distinct action symbols;
5. 5\.𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}, the initial database \(or initial KB\), is a finite set of sentences uniform inS0S\_\{0\}\.

### 2\.2Progression

A progression should retain all proper information, i\.e\., logical entailment in terms of the future of the initial KB\. Lin and ReiterLin and Reiter \([1997](https://arxiv.org/html/2605.12691#bib.bib19)\)provide a model\-theoretical definition of progression and prove that progression is SO definable\. Vassos and LevesqueVassos and Levesque \([2013](https://arxiv.org/html/2605.12691#bib.bib18)\)prove that any correct progression is equivalent to the SO representation ofLin and Reiter \([1997](https://arxiv.org/html/2605.12691#bib.bib19)\)\. Here we use the definition fromVassos and Levesque \([2013](https://arxiv.org/html/2605.12691#bib.bib18)\)\.

Let𝒟s​s​\[α,S0\]\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]be the instantiation of𝒟s​s\\mathcal\{D\}\_\{ss\}wrtα\\alphaandS0S\_\{0\}, i\.e\.𝒟s​s\[α,S0\]⇔⋀F∀x→\.F\(x→,𝑑𝑜\(α,S0\)\)≡ΦF\(x→,α,S0\)\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]\\Leftrightarrow\\bigwedge\_\{F\}\\forall\\vec\{x\}\.F\(\\vec\{x\},\\mathit\{do\}\(\\alpha,S\_\{0\}\)\)\\equiv\\Phi\_\{F\}\(\\vec\{x\},\\alpha,S\_\{0\}\), whereΦF\\Phi\_\{F\}denotes the RHS of the SSA for fluentFF\. LetF1,…​FnF\_\{1\},\\ldots F\_\{n\}be the set of all fluents\. For each fluentFiF\_\{i\}, we introduce a new predicate symbolPiP\_\{i\}\. Letϕ↑S0\\phi\\uparrow S\_\{0\}be the result of replacing everyFi​\(t→,S0\)F\_\{i\}\(\\vec\{t\},S\_\{0\}\)inϕ\\phibyPi​\(t→\)P\_\{i\}\(\\vec\{t\}\)and callPiP\_\{i\}thelifting predicateforFiF\_\{i\}\. For a finite set of formulasΣ\\Sigma, we also useΣ\\Sigmato denote the conjunctions of its elements\.

###### Definition 2\.

Let𝒟\\mathcal\{D\}be a basic action theory,α\\alphaan executable ground action \(under𝒟a​p\\mathcal\{D\}\_\{ap\}\), and𝒟Sα\\mathcal\{D\}\_\{S\_\{\\alpha\}\}a set of \(FO or SO\) sentences uniform inSαS\_\{\\alpha\}\. We say that𝒟Sα\\mathcal\{D\}\_\{S\_\{\\alpha\}\}is a*progression*of𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}wrtα,𝒟\\alpha,\\mathcal\{D\}iff𝒟u​n​a∪𝒟Sα⇔𝒟u​n​a∧\\mathcal\{D\}\_\{una\}\\cup\\mathcal\{D\}\_\{S\_\{\\alpha\}\}\\Leftrightarrow\\mathcal\{D\}\_\{una\}~\\land

∃R→\.\{\(𝒟S0∪𝒟s​s​\[α,S0\]\)↑S0\}​\(P→/R→\)\\exists\\vec\{R\}\.\\\{\(\\mathcal\{D\}\_\{S\_\{0\}\}\\cup\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]\)\\uparrow S\_\{0\}\\\}\(\\vec\{P\}/\\vec\{R\}\)\(1\)whereR→=\{R1,…,Rn\}\\vec\{R\}=\\\{R\_\{1\},\\ldots,R\_\{n\}\\\}are SO predicate variables\.

Def\.[2](https://arxiv.org/html/2605.12691#Thmtheorem2)is correct in the sense that for anyϕ\\phiuniform inSαS\_\{\\alpha\}, if𝒟Sα\\mathcal\{D\}\_\{S\_\{\\alpha\}\}is a progression of𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}wrtα,𝒟\\alpha,\\mathcal\{D\}, then𝒟⊧ϕ​iff​\(𝒟−𝒟S0\)∪𝒟Sα⊧ϕ\\mathcal\{D\}\\models\\phi\\textrm\{ iff \}\(\\mathcal\{D\}\-\\mathcal\{D\}\_\{S\_\{0\}\}\)\\cup\\mathcal\{D\}\_\{S\_\{\\alpha\}\}\\models\\phi\(Vassos and Levesque,[2013](https://arxiv.org/html/2605.12691#bib.bib18), Thm\. 1\)\.

### 2\.3Forgetting

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*\(BAT\-LE\),*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 offorgettingall 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ϕ\\phiand ground atomP​\(t→\)P\(\\vec\{t\}\), letϕ​\[P​\(t→\)\]\\phi\[P\(\\vec\{t\}\)\]be the formula obtained by replacing every occurrence of the formP​\(t→′\)P\(\\vec\{t\}^\{\\prime\}\)inϕ\\phiwith\[t→=t→′∧P​\(t→\)\]∨\[t→≠t→′∧P​\(t→′\)\]\[\\vec\{t\}=\\vec\{t\}^\{\\prime\}\\land P\(\\vec\{t\}\)\]\\vee\[\\vec\{t\}\\neq\\vec\{t\}^\{\\prime\}\\land P\(\\vec\{t\}^\{\\prime\}\)\]\. Clearly,ϕ⇔ϕ​\[P​\(t→\)\]\\phi\\Leftrightarrow\\phi\[P\(\\vec\{t\}\)\]\. Letϕ\+P​\(t→\)\\phi^\{P\(\\vec\{t\}\)\}\_\{\+\}andϕ−P​\(t→\)\\phi^\{P\(\\vec\{t\}\)\}\_\{\-\}be formulas obtained by replacingP​\(t→\)P\(\\vec\{t\}\)inϕ​\[P​\(t→\)\]\\phi\[P\(\\vec\{t\}\)\]withtrueandfalse, respectively\.

###### Theorem 3\(Lin and Reiter \([1994](https://arxiv.org/html/2605.12691#bib.bib7)\)\)\.

LetP​\(t→\)P\(\\vec\{t\}\)be a ground atom,PPa predicate symbol, andϕ\\phia sentence\. Then

- •𝑓𝑜𝑟𝑔𝑒𝑡​\(ϕ,P​\(t→\)\)⇔ϕ\+P​\(t→\)∨ϕ−P​\(t→\)\\mathit\{forget\}\(\\phi,P\(\\vec\{t\}\)\)\\Leftrightarrow\\phi^\{P\(\\vec\{t\}\)\}\_\{\+\}\\vee\\phi^\{P\(\\vec\{t\}\)\}\_\{\-\};
- •𝑓𝑜𝑟𝑔𝑒𝑡\(ϕ,P\)⇔∃R\.ϕ\(P/R\)\\mathit\{forget\}\(\\phi,P\)\\Leftrightarrow\\exists R\.\\phi\(P/R\), whereRRis a SO variable\.

Consequently, progression in Eq\. \([1](https://arxiv.org/html/2605.12691#S2.E1)\) amounts to adding the effects of the action \(𝒟s​s​\[α,S0\]\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]\) and forgetting the truth of fluents at situationS0S\_\{0\}\(∃\\exists\-quantified from the outside\)\. Thus, progression is FO definable in cases where the SO quantifiers in \([1](https://arxiv.org/html/2605.12691#S2.E1)\) can be eliminated\.

W\.l\.o\.g\., we assumeγF±​\(x→,a,s\)\\gamma^\{\\pm\}\_\{F\}\(\\vec\{x\},a,s\)in SSAs are disjunctions of formulas of the form \(one for each action symbolAA\)

∃z→\.\(a=A​\(v→\)∧ϕA±​\(x→,z→,s\)\)\\exists\\vec\{z\}\.\\bigl\(a=A\(\\vec\{v\}\)\\land\\phi^\{\\pm\}\_\{A\}\(\\vec\{x\},\\vec\{z\},s\)\\bigr\)whereA​\(v→\)A\(\\vec\{v\}\)is an action term,v→\\vec\{v\}may contain some variables fromx→\\vec\{x\}, and the remaining variables arez→\\vec\{z\};ϕA±​\(x→,z→,s\)\\phi^\{\\pm\}\_\{A\}\(\\vec\{x\},\\vec\{z\},s\)is a formula uniform insswith no action terms, and where all free variables symbols are amongx→\\vec\{x\},z→\\vec\{z\}, andss\. Under this assumption and𝒟u​n​a\\mathcal\{D\}\_\{una\}, for every ground actionα=A​\(t→\)\\alpha=A\(\\vec\{t\}\),

γF±\(x→,α,S0\)⇔∃z→\.\(t→=v→∧ϕA±\(x→,z→,S0\)\)\.\\gamma^\{\\pm\}\_\{F\}\(\\vec\{x\},\\alpha,S\_\{0\}\)\\Leftrightarrow\\exists\\vec\{z\}\.\\bigl\(\\vec\{t\}=\\vec\{v\}\\land\\phi^\{\\pm\}\_\{A\}\(\\vec\{x\},\\vec\{z\},S\_\{0\}\)\\bigr\)\.\(2\)Henceforth, whenever we refer toγF±​\(x→,α,S0\)\\gamma^\{\\pm\}\_\{F\}\(\\vec\{x\},\\alpha,S\_\{0\}\), we mean the RHS of Eq\. \([2](https://arxiv.org/html/2605.12691#S2.E2)\) and this applies to𝒟s​s​\[α,S0\]\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]as well\.

## 3Size Complexity of Progression

Previous work on the FO progression of acyclic action theoriesLiu and Claßen \([2024](https://arxiv.org/html/2605.12691#bib.bib6)\)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\|ϕ\|\|\\phi\|of a formulaϕ\\phiis the number of atoms \(including equalities\), boolean connectives from\{∧,∨,¬\}\\\{\\land,\\lor,\\lnot\\\}, and quantifiers from\{∃,∀\}\\\{\\exists,\\forall\\\}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, andnotthe 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𝒟Sα\\mathcal\{D\}\_\{S\_\{\\alpha\}\}that replaces𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}in the BAT to reflect the state of the world in the new situation after executing ground actionα\\alpha\. In particular \(cf\. Def\.[2](https://arxiv.org/html/2605.12691#Thmtheorem2)\), the axioms encoding unique names for actions,𝒟u​n​a\\mathcal\{D\}\_\{una\}, 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\.1BAT\-LE

The idea behind local\-effect action theoriesLiu and Lakemeyer \([2009](https://arxiv.org/html/2605.12691#bib.bib2)\)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→\)\\alpha=A\(\\vec\{t\}\)is said to have local effects on a fluentFFifγF±​\(x→,α,S0\)\\gamma^\{\\pm\}\_\{F\}\(\\vec\{x\},\\alpha,S\_\{0\}\)in Eq\. \([2](https://arxiv.org/html/2605.12691#S2.E2)\) is of the form∃z→\.\[t→=v→∧ϕA±​\(z→,S0\)\]\\exists\\vec\{z\}\.\[\\vec\{t\}=\\vec\{v\}\\land\\phi\_\{A\}^\{\\pm\}\(\\vec\{z\},S\_\{0\}\)\]\. We call a BAT a BAT\-LE \(wrtα\\alpha\) ifα\\alphais local\-effect to all fluents\. For such a BAT,𝒟u​n​a\\mathcal\{D\}\_\{una\}impliesγF±​\(x→,α,S0\)≡⋁i\(x→=t→i∧ϕA±​\(x→,S0\)\)\\gamma^\{\\pm\}\_\{F\}\(\\vec\{x\},\\alpha,S\_\{0\}\)\\equiv\\bigvee\_\{i\}\(\\vec\{x\}=\\vec\{t\}\_\{i\}\\land\\phi\_\{A\}^\{\\pm\}\(\\vec\{x\},S\_\{0\}\)\)\(as all possible occurrences ofx→\\vec\{x\}on the RHS of Eq\. \([2](https://arxiv.org/html/2605.12691#S2.E2)\) are amongv→\\vec\{v\}\)\. Hence, there are only finitely many affected fluent instances, i\.e\., the*characteristic set*Ω​\(s\)\\Omega\(s\)given by

\{F\(t→,s\)∣\(x→=t→appears inγF\+\(x→,α,s\)orγF−\(x→,α,s\)\}\.\\displaystyle\\\{F\(\\vec\{t\},s\)\\mid\(\\vec\{x\}=\\vec\{t\}~\\text\{appears in\}~\\gamma\_\{F\}^\{\+\}\(\\vec\{x\},\\alpha,s\)~\\text\{or\}~\\gamma\_\{F\}^\{\-\}\(\\vec\{x\},\\alpha,s\)\\\}\.Let𝒟s​s​\[Ω\]\\mathcal\{D\}\_\{ss\}\[\\Omega\]then be the set of instantiations of𝒟s​s\\mathcal\{D\}\_\{ss\}wrtΩ\\Omega:

𝒟s​s​\[Ω\]=\{F​\(t→,Sα\)≡ΦF​\(t→,α,S0\)∣F​\(t→,s\)∈Ω​\(s\)\},\\displaystyle\\mathcal\{D\}\_\{ss\}\[\\Omega\]=\\\{F\(\\vec\{t\},S\_\{\\alpha\}\)\\equiv\\Phi\_\{F\}\(\\vec\{t\},\\alpha,S\_\{0\}\)\\mid F\(\\vec\{t\},s\)\\in\\Omega\(s\)\\\},whereΦF​\(t→,α,S0\)\\Phi\_\{F\}\(\\vec\{t\},\\alpha,S\_\{0\}\)is the right\-hand side of the SSA forFF\. Liu and LakemeyerLiu and Lakemeyer \([2009](https://arxiv.org/html/2605.12691#bib.bib2)\)observe that for BAT\-LE, forgetting predicates in the progression as in Eq\. \([1](https://arxiv.org/html/2605.12691#S2.E1)\) can be done via forgetting the ground atoms inΩ\\Omega: Ifθ\\thetais a consistent, finite set of ground literals, letϕ​\[θ\]\\phi\[\\theta\]denote the result of replacing every occurrence of an atomP​\(t→\)P\(\\vec\{t\}\)inϕ\\phiby the formula

⋁j=1k\(t→=t→j∧vj\)∨\(⋀j=1kt→≠t→j\)∧P​\(t→\),\\displaystyle\\bigvee\_\{j=1\}^\{k\}\(\\vec\{t\}=\\vec\{t\}\_\{j\}\\land v\_\{j\}\)\\lor\(\\bigwedge\_\{j=1\}^\{k\}\\vec\{t\}\\neq\\vec\{t\}\_\{j\}\)\\land P\(\\vec\{t\}\),\(3\)where forj=1,…,kj=1,\\dots,k,θ\\thetaspecifies truth valuevjv\_\{j\}forP​\(t→j\)P\(\\vec\{t\}\_\{j\}\)\. Theorem 3\.6 ofLiu and Lakemeyer \([2009](https://arxiv.org/html/2605.12691#bib.bib2)\)states that the following is then a progression of𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}wrtα,𝒟\\alpha,\\mathcal\{D\}:

⋀𝒟u​n​a∧⋁θ∈ℳ​\(Ω​\(S0\)\)\(𝒟S0∪𝒟s​s​\[Ω\]\)​\[θ\]​\(S0/Sα\)\\bigwedge\\mathcal\{D\}\_\{una\}\\land\\bigvee\_\{\\theta\\in\{\\cal M\}\(\\Omega\(S\_\{0\}\)\)\}\(\\mathcal\{D\}\_\{S\_\{0\}\}\\cup\\mathcal\{D\}\_\{ss\}\[\\Omega\]\)\[\\theta\]\(S\_\{0\}/S\_\{\\alpha\}\)\(4\)Here,ℳ​\(Ω​\(S0\)\)\{\\cal M\}\(\\Omega\(S\_\{0\}\)\)denotes the set of all maximal consistent sets of literals over the atoms inΩ​\(S0\)\\Omega\(S\_\{0\}\)\. The big disjunction in Eq\. \([4](https://arxiv.org/html/2605.12691#S3.E4)\) essentially amounts to𝑓𝑜𝑟𝑔𝑒𝑡​\(𝒟S0∪𝒟s​s​\[Ω\],ΩS0\)\\mathit\{forget\}\(\\mathcal\{D\}\_\{S\_\{0\}\}\\cup\\mathcal\{D\}\_\{ss\}\[\\Omega\],\\Omega\_\{S\_\{0\}\}\)\(which means iteratively forgetting atoms inΩ​\(S0\)\\Omega\(S\_\{0\}\)\)\. The claim in the following theorem was already stated inLiu and Lakemeyer \([2009](https://arxiv.org/html/2605.12691#bib.bib2)\), however, without a proof\.

###### Theorem 4\.

If𝒟\\mathcal\{D\}is BAT\-LE wrt ground actionα\\alpha, then its progression can be represented by a FO theory of sizeO​\(2c​\(n\+m\)\)O\(2^\{c\}\(n\+m\)\), whereccis the size of the characteristic set,nnis the size of𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}, andmmis the size of𝒟s​s\\mathcal\{D\}\_\{ss\}\.

###### Proof\.

The size of𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}isnnby assumption, and the size of𝒟s​s​\[Ω\]\\mathcal\{D\}\_\{ss\}\[\\Omega\]is bounded byc​m\+c−1cm\+c\-1, since there areccmany formulas in𝒟s​s​\[Ω\]\\mathcal\{D\}\_\{ss\}\[\\Omega\], each of size less or equal tomm, with\(c−1\)\(c\-1\)conjunction symbols between them\. Ifϕ\\phidenotes𝒟S0∪𝒟s​s​\[Ω\]\\mathcal\{D\}\_\{S\_\{0\}\}\\cup\\mathcal\{D\}\_\{ss\}\[\\Omega\], we hence have\|ϕ\|≤n\+c​m\+c\|\\phi\|\\leq n\+cm\+c\.

Observe that for anyθ∈ℳ​\(Ω​\(S0\)\)\\theta\\in\{\\cal M\}\(\\Omega\(S\_\{0\}\)\), the number of elements inθ\\thetais the same as the number of elements inΩ\\Omega, i\.e\.,cc\. In particular, in \([3](https://arxiv.org/html/2605.12691#S3.E3)\),k≤ck\\leq c\. Ifaadenotes the maximal arity of any predicatePPinϕ\\phi,t→=t→j\\vec\{t\}=\\vec\{t\}\_\{j\}abbreviates a formula of size less than2​a2a, and so the size of the formula in \([3](https://arxiv.org/html/2605.12691#S3.E3)\) is bounded by4​c​a\+4​c\+34ca\+4c\+3\. Therefore, for anyϕ\\phi,\|ϕ​\[θ\]\|≤\(4​c​a\+4​c\+3\)​\|ϕ\|\|\\phi\[\\theta\]\|\\leq\(4ca\+4c\+3\)\|\\phi\|\.

Finally, observe that the step\(S0/Sα\)\(S\_\{0\}/S\_\{\\alpha\}\)substitutes one constant by another, and hence does not change the size of the formula\. Also, there are2c2^\{c\}manyθ\\theta’s inℳ​\(Ω​\(S0\)\)\{\\cal M\}\(\\Omega\(S\_\{0\}\)\)\. As argued above, the size of𝒟u​n​a\\mathcal\{D\}\_\{una\}can be ignored\. In summary, we can estimate the size of the progression to be no more than2c⋅\(n\+c​m\+c\)⋅\(4​c​a\+4​c\+3\)2^\{c\}\\cdot\(n\+cm\+c\)\\cdot\(4ca\+4c\+3\)\. Sinceaais constant under the assumption of a fixed vocabulary, we get that the size of the progression is inO​\(2c​\(n\+m\)\)O\(2^\{c\}\(n\+m\)\)\. ∎

We remark thatcccan be bounded by a constant\. Note that the elements ofΩ​\[S0\]\\Omega\[S\_\{0\}\]are of the formF​\(t→,S0\)F\(\\vec\{t\},S\_\{0\}\), whereFFis a local\-effect fluent, and thet→\\vec\{t\}have to be chosen from the arguments of ground actionα\\alpha\. Therefore, ifllis the number of local\-effect fluents,bbis the arity ofα\\alpha, andaais again the maximal arity among predicates,c≤l⋅bac\\leq l\\cdot b^\{a\}, where all ofll,aa, andbbare 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\.2BAT\-NR

To facilitate global effects, BAT\-NR relaxes the restriction on SSAs but imposes additional assumptions on𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}so that one can use a variant Ackermann’s LemmaAckermann \([1935](https://arxiv.org/html/2605.12691#bib.bib16)\)to eliminate SO quantifiers\. Formally, a finite theoryTTis*semi\-definitional*wrt a predicatePPif the only occurrence ofPPinTTis of the formP​\(x→\)⊃ϕ​\(x→\)P\(\\vec\{x\}\)\\supset\\phi\(\\vec\{x\}\)orψ​\(x→\)⊃P​\(x→\)\\psi\(\\vec\{x\}\)\\supset P\(\\vec\{x\}\)\.ϕ\\phi\(respectivelyψ\\psi\) is called a necessary \(sufficient\) condition ofPP\. LetWSCP\\mathrm\{WSC\}\_\{P\}be the set formulasψ​\(x→\)\\psi\(\\vec\{x\}\)such thatψ​\(x→\)⊃P​\(x→\)\\psi\(\\vec\{x\}\)\\supset P\(\\vec\{x\}\)is inTT, andSNCP\\mathrm\{SNC\}\_\{P\}be the set of formulasϕ​\(x→\)\\phi\(\\vec\{x\}\)withP​\(x→\)⊃ϕ​\(x→\)P\(\\vec\{x\}\)\\supset\\phi\(\\vec\{x\}\)inTT\. Then the following holds:

###### Theorem 5\(Liu and Lakemeyer \([2009](https://arxiv.org/html/2605.12691#bib.bib2)\)\)\.

LetTTbe finite and semi\-definitional wrtPP, andT′T^\{\\prime\}the set of sentences inTTnot mentioningPP\. Then𝑓𝑜𝑟𝑔𝑒𝑡\(T,P\)⇔T′∧⋀ψ∈WSCP,ϕ∈SNCP∀x→\.ψ\(x→\)⊃ϕ\(x→\)\\mathit\{forget\}\(T,P\)\\Leftrightarrow T^\{\\prime\}\\land\\bigwedge\_\{\\psi\\in\\mathrm\{WSC\}\_\{P\},\\phi\\in\\mathrm\{SNC\}\_\{P\}\}\\forall\\vec\{x\}\.\\psi\(\\vec\{x\}\)\\supset\\phi\(\\vec\{x\}\)\.

###### Proposition 6\.

In any model of𝒟\\mathcal\{D\}, the SSA forFFinstantiated by ground actionα\\alpha,𝒟s​sF​\[α,S0\]\\mathcal\{D\}^\{F\}\_\{ss\}\[\\alpha,S\_\{0\}\], is equivalent to:

¬γF\+​\(x→,α,S0\)∧F​\(x→,Sα\)⊃F​\(x→,S0\)\\displaystyle\\neg\\gamma^\{\+\}\_\{F\}\(\\vec\{x\},\\alpha,S\_\{0\}\)\\wedge F\(\\vec\{x\},S\_\{\\alpha\}\)\\supset F\(\\vec\{x\},S\_\{0\}\)\(5a\)F​\(x→,S0\)⊃γF−​\(x→,α,S0\)∨F​\(x→,Sα\)\\displaystyle F\(\\vec\{x\},S\_\{0\}\)\\supset\\gamma^\{\-\}\_\{F\}\(\\vec\{x\},\\alpha,S\_\{0\}\)\\vee F\(\\vec\{x\},S\_\{\\alpha\}\)\(5b\)γF\+​\(x→,α,S0\)⊃F​\(x→,Sα\)\\displaystyle\\gamma^\{\+\}\_\{F\}\(\\vec\{x\},\\alpha,S\_\{0\}\)\\supset F\(\\vec\{x\},S\_\{\\alpha\}\)\(5c\)γF−​\(x→,α,S0\)⊃¬F​\(x→,Sα\)\\displaystyle\\gamma^\{\-\}\_\{F\}\(\\vec\{x\},\\alpha,S\_\{0\}\)\\supset\\neg F\(\\vec\{x\},S\_\{\\alpha\}\)\(5d\)

We say a formulaϕ\\phiis semi\-definitional wrt a fluentFFifϕ↑S0\\phi\\uparrow S\_\{0\}is semi\-definitional wrtFF’s lifting predicate\. The proposition suggests that𝒟s​sF​\[α,S0\]\\mathcal\{D\}^\{F\}\_\{ss\}\[\\alpha,S\_\{0\}\]for every fluentFFis semi\-definitional wrtFF\. Hence, if𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}is also semi\-definitional wrt fluents, one can use Thm\.[5](https://arxiv.org/html/2605.12691#Thmtheorem5)to forget their lifting predicates in Eq\. \([1](https://arxiv.org/html/2605.12691#S2.E1)\), which is the idea behind normal actions and their progression\. For an actionα\\alpha, we distinguish local\-effect fluentsLE​\(α\)\\mathrm\{LE\}\(\\alpha\)on the one hand \(whose SSAs are as in BAT\-LE\), and non\-local effect fluentsNLE​\(α\)\\mathrm\{NLE\}\(\\alpha\)on the other hand\. Normal actions then require that for allF∈NLE​\(α\)F\\in\\mathrm\{NLE\}\(\\alpha\), fluents occurring inγF±\\gamma^\{\\pm\}\_\{F\}can only be inLE​\(α\)\\mathrm\{LE\}\(\\alpha\)\. We call a BAT𝒟\\mathcal\{D\}a BAT\-NR \(wrt actionα\\alpha\) ifα\\alphais normal and𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}is semi\-definitional wrt fluents inNLE​\(α\)\\mathrm\{NLE\}\(\\alpha\)\. For such a BAT, one can forget lifting predicates of fluents inNLE​\(α\)\\mathrm\{NLE\}\(\\alpha\)by Thm\.[5](https://arxiv.org/html/2605.12691#Thmtheorem5)and thereafter fluents inLE​\(α\)\\mathrm\{LE\}\(\\alpha\)as in Eq\. \([4](https://arxiv.org/html/2605.12691#S3.E4)\)\.

###### Theorem 7\.

If𝒟\\mathcal\{D\}is BAT\-NR wrt ground actionα\\alpha, the result of forgetting the lifting predicates for all fluents inNLE​\(α\)\\mathrm\{NLE\}\(\\alpha\)in\(𝒟S0∪𝒟s​s​\[α,S0\]\)↑S0\(\\mathcal\{D\}\_\{S\_\{0\}\}\\cup\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]\)\\uparrow S\_\{0\}can be represented by a FO theory whose size is inO​\(\(n\+m\)2\)O\(\(n\+m\)^\{2\}\), wherennis the size of𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}, andmmis the size of𝒟s​s\\mathcal\{D\}\_\{ss\}\.

###### Proof\.

First, note that we can ignore the lifting operator↑S0\\uparrow S\_\{0\}here, since it only replaces atoms by other atoms, and thus does not affect the size of a formula\. Now, assume that for fluentsF∈NLE​\(α\)F\\in\\mathrm\{NLE\}\(\\alpha\), axioms in𝒟s​s​\[α,S0\]\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]are represented according to Prop\.[6](https://arxiv.org/html/2605.12691#Thmtheorem6)\. Note that \([5a](https://arxiv.org/html/2605.12691#S3.E5.1)\) and \([5b](https://arxiv.org/html/2605.12691#S3.E5.2)\) are semi\-definitional wrtF​\(x→,S0\)F\(\\vec\{x\},S\_\{0\}\), and \([5c](https://arxiv.org/html/2605.12691#S3.E5.3)\) and \([5d](https://arxiv.org/html/2605.12691#S3.E5.4)\) do not mentionF​\(x→,S0\)F\(\\vec\{x\},S\_\{0\}\)\. Theorem[5](https://arxiv.org/html/2605.12691#Thmtheorem5)is hence applicable to𝒟S0∪𝒟s​s​\[α,S0\]\\mathcal\{D\}\_\{S\_\{0\}\}\\cup\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]\. Intuitively, the set of semi\-definitional formulas in𝒟S0∪𝒟s​s​\[α,S0\]\\mathcal\{D\}\_\{S\_\{0\}\}\\cup\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]can be represented as a directed graph, where any formulaψ​\(x→\)⊃ϕ​\(x→\)\\psi\(\\vec\{x\}\)\\supset\\phi\(\\vec\{x\}\)corresponds to an edge fromψ​\(x→\)\\psi\(\\vec\{x\}\)toϕ​\(x→\)\\phi\(\\vec\{x\}\)\. Forgetting the lifting predicate for a fluentF∈NLE​\(α\)F\\in\\mathrm\{NLE\}\(\\alpha\)then amounts to eliminating the node forF​\(x→,S0\)F\(\\vec\{x\},S\_\{0\}\), “bypassing” all involved edges, i\.e\., every pair of ingoing edgeψ​\(x→\)⊃F​\(x→,S0\)\\psi\(\\vec\{x\}\)\\supset F\(\\vec\{x\},S\_\{0\}\)and outgoing edgeF​\(x→,S0\)⊃ϕ​\(x→\)F\(\\vec\{x\},S\_\{0\}\)\\supset\\phi\(\\vec\{x\}\)is replaced by a new edgeψ​\(x→\)⊃ϕ​\(x→\)\\psi\(\\vec\{x\}\)\\supset\\phi\(\\vec\{x\}\)\. This elimination operation is performed iteratively for allF∈NLE​\(α\)F\\in\\mathrm\{NLE\}\(\\alpha\)\(in any order\), leaving only nodes that correspond to conditions that donotmention 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 byn\+mn\+m, the size of the theory representing all combinations of implications between them is inO​\(\(n\+m\)2\)O\(\(n\+m\)^\{2\}\)\. Moreover, the size of the original formulas in𝒟S0∪𝒟s​s​\[α,S0\]\\mathcal\{D\}\_\{S\_\{0\}\}\\cup\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]that do not mention any of the NLE fluents \(including \([5c](https://arxiv.org/html/2605.12691#S3.E5.3)\) and \([5d](https://arxiv.org/html/2605.12691#S3.E5.4)\)\) is bounded byn\+mn\+mas well\. All in all, the size of the resulting theory is thus inO​\(\(n\+m\)2\)O\(\(n\+m\)^\{2\}\)\. ∎

According toLiu and Lakemeyer \([2009](https://arxiv.org/html/2605.12691#bib.bib2)\), the progression of a BAT\-NR through an actionα\\alphais obtained by first forgetting the \(lifting predicates\) of the fluents inNLE​\(α\)\\mathrm\{NLE\}\(\\alpha\), and afterwards forgetting the remaining atoms over the fluents inLE​\(α\)\\mathrm\{LE\}\(\\alpha\)\. We can estimate the size of the resulting theory by combining the results from Theorems[4](https://arxiv.org/html/2605.12691#Thmtheorem4)and[7](https://arxiv.org/html/2605.12691#Thmtheorem7), giving:

###### Corollary 8\.

If𝒟\\mathcal\{D\}is BAT\-NR wrt ground actionα\\alpha, then its progression can be represented by a FO theory of sizeO​\(2c​\(n\+m\)2\)O\(2^\{c\}\(n\+m\)^\{2\}\), whereccis the size of the characteristic set,nnis the size of𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}, andmmis the size of𝒟s​s\\mathcal\{D\}\_\{ss\}\.

### 3\.3BAT\-AC

While normal action theories allow for non\-local effects of a certain form, they include the requirement that for BAT\-NR, the effect conditionsγF±\\gamma^\{\\pm\}\_\{F\}for a fluentFFmay only mention local\-effect fluents\. This assumption ensures that forgetting the lifting predicate forFFwill not generate formulas that mention the lifting predicate of another NLE fluentF′F^\{\\prime\}, which might not have the right \(semi\-definitional\) form to proceed with forgettingF′F^\{\\prime\}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 theoriesLiu and Claßen \([2024](https://arxiv.org/html/2605.12691#bib.bib6)\)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±\\gamma^\{\\pm\}\_\{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→\)\\phi\(\\vec\{x\}\)is said to be in*good form*wrt a predicatePPif it is of the form

\[ψ​\(x→\)∨P​\(t→\)\]∧\[ψ′​\(x→\)∨¬P​\(t→\)\]∧ψ′′​\(x→\)\[\\psi\(\\vec\{x\}\)\\vee P\(\\vec\{t\}\)\]\\land\[\\psi^\{\\prime\}\(\\vec\{x\}\)\\vee\\neg P\(\\vec\{t\}\)\]\\land\\psi^\{\\prime\\prime\}\(\\vec\{x\}\)\(6\)whereψ,ψ′,ψ′′\\psi,\\psi^\{\\prime\},\\psi^\{\\prime\\prime\}contain noPP, and terms int→\\vec\{t\}are either ground terms or free variables amongx→\\vec\{x\}\.

###### Proposition 9\(Liu and Claßen \([2024](https://arxiv.org/html/2605.12691#bib.bib6)\)\)\.

Ifϕ​\(x→\)\\phi\(\\vec\{x\}\)is in good form wrtPP, then

1. 1\.ϕ​\(x→\)\\phi\(\\vec\{x\}\)can be rewritten to be semi\-definitional wrtPP;
2. 2\.¬ϕ​\(x→\)\\neg\\phi\(\\vec\{x\}\)can be rewritten to be in good form wrtPP\.

Now, given SSAs𝒟s​s\\mathcal\{D\}\_\{ss\}and a ground actionα\\alpha, the*dependency graph*GGfor𝒟s​s\\mathcal\{D\}\_\{ss\}wrtα\\alphais a directed graph whose vertices are the set of fluents and there is an edgeF→F′F\\rightarrow F^\{\\prime\}for two fluentsF,F′F,F^\{\\prime\}iffF∈NLE​\(α\)F\\in\\mathrm\{NLE\}\(\\alpha\)andF′F^\{\\prime\}appears inγF±\\gamma^\{\\pm\}\_\{F\}\. A ground actionα\\alphaisacyclic\(or has acyclic effects\) if 1\) its dependency graphGGis acyclic, i\.e\., a DAG; and 2\) for each fluentFF, there are*at most two*fluentsF′,F′′F^\{\\prime\},F^\{\\prime\\prime\}inNLE​\(α\)\\mathrm\{NLE\}\(\\alpha\)such thatF→F′F\\rightarrow F^\{\\prime\}andF→F′′F\\rightarrow F^\{\\prime\\prime\}, whereγF\+\\gamma^\{\+\}\_\{F\}andγF−\\gamma^\{\-\}\_\{F\}are in good form wrtF′F^\{\\prime\}andF′′F^\{\\prime\\prime\}, respectively\.

We call a BAT a BAT\-AC \(wrtα\\alpha\), ifα\\alphais acyclic and𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}is*separably semi\-definitional*wrtNLE​\(α\)\\mathrm\{NLE\}\(\\alpha\), that is, each sentence in𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}mentions at most one fluentFFinNLE​\(α\)\\mathrm\{NLE\}\(\\alpha\)and is semi\-definitional wrtFF\.Liu and Claßen \([2024](https://arxiv.org/html/2605.12691#bib.bib6)\)showed that if a BAT𝒟\\mathcal\{D\}is a BAT\-AC, the progression of𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}wrtα,𝒟\\alpha,\\mathcal\{D\}is FO definable\. This is because for anyF,F′∈NLE​\(α\)F,F^\{\\prime\}\\in\\mathrm\{NLE\}\(\\alpha\), even if forgetting the lifting predicate ofFFwill possibly generate new formulas that mentionF′F^\{\\prime\}, the assumption ofγF±\\gamma^\{\\pm\}\_\{F\}being in good form wrtF′F^\{\\prime\}ensures that the new formulas can be rewritten to be semi\-definitional wrtF′F^\{\\prime\}again\. Hence, one can recursively forget lifting predicates forF∈NLE​\(α\)F\\in\\mathrm\{NLE\}\(\\alpha\)\(following the order of the DAG\) and later forget lifting predicates ofF∈LE​\(α\)F\\in\\mathrm\{LE\}\(\\alpha\)as in Eq\. \([4](https://arxiv.org/html/2605.12691#S3.E4)\)\. For analyzing the size of the resulting theory, we need the following:

###### Definition 10\.

Ifϕ​\(x→\)\\phi\(\\vec\{x\}\)is in good form wrtPP, i\.e\.,ϕ​\(x→\):=\(ψ​\(x→\)∨P​\(t→\)\)∧\(ψ′​\(x→\)∨¬P​\(t→\)\)∧ψ′′​\(x→\)\\phi\(\\vec\{x\}\):=\(\\psi\(\\vec\{x\}\)\\lor P\(\\vec\{t\}\)\)\\land\(\\psi^\{\\prime\}\(\\vec\{x\}\)\\lor\\lnot P\(\\vec\{t\}\)\)\\land\\psi^\{\\prime\\prime\}\(\\vec\{x\}\), we define\|ϕ\|P=max⁡\{\|ψ\|,\|ψ′\|,\|ψ′′\|\}\|\\phi\|\_\{P\}=\\max\\\{\|\\psi\|,\|\\psi^\{\\prime\}\|,\|\\psi^\{\\prime\\prime\}\|\\\}as thecondition size ofϕ\\phiwrtPP\.

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 that for eachF∈NLE​\(α\)F\\in\\mathrm\{NLE\}\(\\alpha\),𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}containsexactly oneaxiom

ΔF=\(𝑁𝑊𝑆F​\(x→\)∨F​\(x→,S0\)\)∧\(𝑆𝑁𝐶F​\(x→\)∨¬F​\(x→,S0\)\)\\displaystyle\\Delta\_\{F\}=\\left\(\\mathit\{NWS\}\_\{F\}\(\\vec\{x\}\)\\lor F\(\\vec\{x\},S\_\{0\}\)\\right\)\\land\\left\(\\mathit\{SNC\}\_\{F\}\(\\vec\{x\}\)\\lor\\lnot F\(\\vec\{x\},S\_\{0\}\)\\right\)This is without loss of generality: If𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}contains multiple semi\-definitional formulas forFF, let𝑁𝑊𝑆F\\mathit\{NWS\}\_\{F\}be the negation of the weakest sufficient condition, and𝑆𝑁𝐶F\\mathit\{SNC\}\_\{F\}the strongest necessary condition\. Observe that with the implicit negation in𝑁𝑊𝑆\\mathit\{NWS\},ΔF\\Delta\_\{F\}is indeed in semi\-definitional form, and such formulas can be assumed to be of good form \([6](https://arxiv.org/html/2605.12691#S3.E6)\)\. Also, this assumption has no impact on size or condition size:

###### Proposition 11\.

Ifϕ1​\(x→\),ϕ2​\(x→\),…,ϕn​\(x→\)\\phi\_\{1\}\(\\vec\{x\}\),\\phi\_\{2\}\(\\vec\{x\}\),\\dots,\\phi\_\{n\}\(\\vec\{x\}\)are all semi\-definitional wrt predicatePP, thenϕ1​\(x→\)∧ϕ2​\(x→\)∧⋯∧ϕn​\(x→\)\\phi\_\{1\}\(\\vec\{x\}\)\\land\\phi\_\{2\}\(\\vec\{x\}\)\\land\\dots\\land\\phi\_\{n\}\(\\vec\{x\}\)can be rewritten to a single equivalent formulaφ​\(x→\)\\varphi\(\\vec\{x\}\)such that\|φ​\(x→\)\|≤\|⋀iϕi​\(x→\)\|\|\\varphi\(\\vec\{x\}\)\|\\leq\|\\bigwedge\_\{i\}\\phi\_\{i\}\(\\vec\{x\}\)\|and\|φ​\(x→\)\|P≤\|⋀iϕi​\(x→\)\|P\|\\varphi\(\\vec\{x\}\)\|\_\{P\}\\leq\|\\bigwedge\_\{i\}\\phi\_\{i\}\(\\vec\{x\}\)\|\_\{P\}\.

Next, we consider formulas in good form and how rewriting them as in Prop\.[9](https://arxiv.org/html/2605.12691#Thmtheorem9)affects the size of the result:

###### Proposition 12\.

Ifϕ​\(x→\)\\phi\(\\vec\{x\}\)is in good form wrtPP, then

1. 1\.ϕ​\(x→\)\\phi\(\\vec\{x\}\)can be rewritten toφ​\(y→\)\\varphi\(\\vec\{y\}\)that is semi\-definitional wrtP​\(y→\)P\(\\vec\{y\}\), moreover, ifa=max⁡\{\|x→\|,\|y→\|\}a=\\max\\\{\|\\vec\{x\}\|,\|\\vec\{y\}\|\\\}, then\|φ​\(y→\)\|≤\|ϕ​\(x→\)\|\+7​a\+2\|\\varphi\(\\vec\{y\}\)\|\\leq\|\\phi\(\\vec\{x\}\)\|\+7a\+2and\|φ​\(y→\)\|P≤\|ϕ​\(x→\)\|P\+3​a\+1\|\\varphi\(\\vec\{y\}\)\|\_\{P\}\\leq\|\\phi\(\\vec\{x\}\)\|\_\{P\}\+3a\+1;
2. 2\.¬ϕ​\(x→\)\\lnot\\phi\(\\vec\{x\}\)can be rewritten toφ​\(x→\)\\varphi\(\\vec\{x\}\)that is in good form wrtPPwith\|φ​\(x→\)\|≤3​\|ϕ​\(x→\)\|\|\\varphi\(\\vec\{x\}\)\|\\leq 3\|\\phi\(\\vec\{x\}\)\|and\|φ​\(x→\)\|P≤3​\|ϕ​\(x→\)\|P\+2\|\\varphi\(\\vec\{x\}\)\|\_\{P\}\\leq 3\|\\phi\(\\vec\{x\}\)\|\_\{P\}\+2;
3. 3\.ifψ​\(x→\)\\psi\(\\vec\{x\}\)mentions noPP, thenϕ​\(x→\)∨ψ​\(x→\)\\phi\(\\vec\{x\}\)\\lor\\psi\(\\vec\{x\}\)can be rewritten to a formulaφ​\(x→\)\\varphi\(\\vec\{x\}\)in good form wrtPP, where\|φ​\(x→\)\|=\|ϕ​\(x→\)\|\+3​\|ψ​\(x→\)\|\+3\|\\varphi\(\\vec\{x\}\)\|=\|\\phi\(\\vec\{x\}\)\|\+3\|\\psi\(\\vec\{x\}\)\|\+3and\|φ​\(x→\)\|P=\|ϕ​\(x→\)\|P\+\|ψ​\(x→\)\|\+1\|\\varphi\(\\vec\{x\}\)\|\_\{P\}=\|\\phi\(\\vec\{x\}\)\|\_\{P\}\+\|\\psi\(\\vec\{x\}\)\|\+1\.

Then we have:

###### Theorem 13\.

If𝒟\\mathcal\{D\}is BAT\-AC wrt ground actionα\\alpha, the result of forgetting the lifting predicates for all fluents inNLE​\(α\)\\mathrm\{NLE\}\(\\alpha\)in\(𝒟S0∪𝒟s​s​\[α,S0\]\)↑S0\(\\mathcal\{D\}\_\{S\_\{0\}\}\\cup\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]\)\\uparrow S\_\{0\}can be represented by a FO theory whose size is inO​\(2d​\(n\+m\)\)O\(2^\{d\}\(n\+m\)\), whereddis the depth of the dependency graph,nnthe size of𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}, andmmthe size of𝒟s​s\\mathcal\{D\}\_\{ss\}\.

###### Proof\.

The proof for Theorem 3 inLiu and Claßen \([2024](https://arxiv.org/html/2605.12691#bib.bib6)\)makes an inductive argument that one can forget fluentsF∈NLE​\(α\)F\\in\\mathrm\{NLE\}\(\\alpha\)iteratively while maintaining the required form, as long as one forgets all predecessors ofFFin the dependency graph before forgettingFFitself\. By Prop\.[6](https://arxiv.org/html/2605.12691#Thmtheorem6)and Thm\.[5](https://arxiv.org/html/2605.12691#Thmtheorem5), forgetting any suchFFamounts to replacing the correspondingΔF\\Delta\_\{F\}by the following \(parameters ofγF±\\gamma^\{\\pm\}\_\{F\}are omitted\):

𝑁𝑊𝑆F​\(x→\)∨𝑆𝑁𝐶F​\(x→\)\\displaystyle\\mathit\{NWS\}\_\{F\}\(\\vec\{x\}\)\\lor\\mathit\{SNC\}\_\{F\}\(\\vec\{x\}\)\(7a\)¬γF\+∨F​\(x→,Sα\)\\displaystyle\\lnot\\gamma\_\{F\}^\{\+\}\\lor F\(\\vec\{x\},S\_\{\\alpha\}\)\(3​k\+3​a\+5\)\\displaystyle\(3k\+3a\+5\)\(7b\)¬γF−∨¬F​\(x→,Sα\)\\displaystyle\\lnot\\gamma\_\{F\}^\{\-\}\\lor\\lnot F\(\\vec\{x\},S\_\{\\alpha\}\)\(3​k\+3​a\+6\)\\displaystyle\(3k\+3a\+6\)\(7c\)γF\+∨¬F​\(x→,Sα\)∨𝑆𝑁𝐶F​\(x→\)\\displaystyle\\gamma\_\{F\}^\{\+\}\\lor\\lnot F\(\\vec\{x\},S\_\{\\alpha\}\)\\lor\\mathit\{SNC\}\_\{F\}\(\\vec\{x\}\)\(wF\+k\+3​a\+5\)\\displaystyle\(w\_\{F\}\+k\+3a\+5\)\(7d\)𝑁𝑊𝑆F​\(x→\)∨γF−∨F​\(x→,Sα\)\\displaystyle\\mathit\{NWS\}\_\{F\}\(\\vec\{x\}\)\\lor\\gamma\_\{F\}^\{\-\}\\lor F\(\\vec\{x\},S\_\{\\alpha\}\)\(wF\+k\+3​a\+4\)\\displaystyle\(w\_\{F\}\+k\+3a\+4\)\(7e\)By definition, there are at most two other NLE fluentsF1,F2F\_\{1\},F\_\{2\}withF→F1F\\rightarrow F\_\{1\}andF→F2F\\rightarrow F\_\{2\}, whereF1F\_\{1\}only occurs inγF\+\\gamma\_\{F\}^\{\+\}, andF2F\_\{2\}only inγF−\\gamma\_\{F\}^\{\-\}\. \([7b](https://arxiv.org/html/2605.12691#S3.E7.2)\) and \([7d](https://arxiv.org/html/2605.12691#S3.E7.4)\) will subsequently be incorporated into the new axiomΔF1\\Delta\_\{F\_\{1\}\}, and \([7c](https://arxiv.org/html/2605.12691#S3.E7.3)\) and \([7e](https://arxiv.org/html/2605.12691#S3.E7.5)\) into the new axiomΔF2\\Delta\_\{F\_\{2\}\}\. IfwFw\_\{F\}is the condition size of the updatedΔF\\Delta\_\{F\}andkkthe maximal size of an SSA for any NLE fluent, then by Prop\.[12](https://arxiv.org/html/2605.12691#Thmtheorem12), upper bounds for the condition sizes of formulas \([7b](https://arxiv.org/html/2605.12691#S3.E7.2)\)–\([7e](https://arxiv.org/html/2605.12691#S3.E7.5)\) after rewriting them to be in good form wrt\.F1,F2F\_\{1\},F\_\{2\}are as stated above in parentheses\. Ifwwis an upper bound for the condition size of anyoriginalΔF\\Delta\_\{F\}axiom, the condition size for theupdatedΔF′\\Delta\_\{F^\{\\prime\}\}is bounded according to

wF′\\displaystyle w\_\{F^\{\\prime\}\}≤w\+∑F→F′\(wF\+4​k\+6​a\+10\)\.\\displaystyle\\leq w\+\\sum\_\{F\\rightarrow F^\{\\prime\}\}\(w\_\{F\}\+4k\+6a\+10\)\.\(8\)The sum of the sizes of \([7a](https://arxiv.org/html/2605.12691#S3.E7.1)\)–\([7e](https://arxiv.org/html/2605.12691#S3.E7.5)\) over all NLE fluentsFFgives an upper bound for the size of the progression\. Observe that the total size ofγF±\\gamma\_\{F\}^\{\\pm\},F​\(x→,Sα\)F\(\\vec\{x\},S\_\{\\alpha\}\)atoms, and boolean connectives is less than\|𝒟s​sF​\[α,S0\]\|\|\\mathcal\{D\}\_\{ss\}^\{F\}\[\\alpha,S\_\{0\}\]\|as in Prop\.[6](https://arxiv.org/html/2605.12691#Thmtheorem6), i\.e\., less thanmmsummed over all NLE fluents\. This leaves two occurrences of𝑁𝑊𝑆F​\(x→\)\\mathit\{NWS\}\_\{F\}\(\\vec\{x\}\)and two of𝑆𝑁𝐶F​\(x→\)\\mathit\{SNC\}\_\{F\}\(\\vec\{x\}\), each of size≤wF\\leq w\_\{F\}, summing up toS=4​∑F∈NLE​\(α\)wFS=4\\sum\_\{F\\in\\mathrm\{NLE\}\(\\alpha\)\}w\_\{F\}\. To determine the sum of allwFw\_\{F\}, we use the intuition that the linear recurrence in \([8](https://arxiv.org/html/2605.12691#S3.E8)\) can be unrolled along all source\-to\-node paths\. Intuitively, each nodeFFstarts with awFw\_\{F\}“weight” ofwwand addswF\+4​k\+6​a\+10w\_\{F\}\+4k\+6a\+10to each of its children\. This contribution is added multiple times, namely for each path starting inFF\. As the out\-degree of nodes is≤2\\leq 2, the number of distinct paths starting inFFis≤2d\+1\\leq 2^\{d\+1\}\. Ifllis the number of NLE fluents, we getS≤4⋅2d\+1⋅l⋅\(w\+4​k\+6​a\+10\)S\\leq 4\\cdot 2^\{d\+1\}\\cdot l\\cdot\(w\+4k\+6a\+10\)\. Sinceaais a constant,l⋅w∈O​\(n\)l\\cdot w\\in O\(n\), andl⋅k∈O​\(m\)l\\cdot k\\in O\(m\), the claim follows\. ∎

Combining the above theorem with Theorem[4](https://arxiv.org/html/2605.12691#Thmtheorem4)again yields:

###### Corollary 14\.

If𝒟\\mathcal\{D\}is BAT\-AC wrt ground actionα\\alpha, then its progression can be represented by a FO theory of sizeO​\(2c\+d​\(n\+m\)\)O\(2^\{c\+d\}\(n\+m\)\), whereccis the size of the characteristic set,ddis the depth of the dependency graph,nnis the size of𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}, andmmis the size of𝒟s​s\\mathcal\{D\}\_\{ss\}\.

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 formF​\(x→,S0\)⊃G​\(x→,S0\)F\(\\vec\{x\},S\_\{0\}\)\\supset G\(\\vec\{x\},S\_\{0\}\), where bothFFandGGare NLE fluents, whereas BAT\-AC requires a strict separation so that a semi\-definitional axiom forFFdoes not mention any NLE fluentGG, 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 edgeF→GF\\rightarrow Gis between an NLE fluentFFand a LE fluentGG\. The size of the progression then is inO​\(2c​\(n\+m\)\)O\(2^\{c\}\(n\+m\)\)\.

## 4The 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𝒯\\mathcal\{T\}is called*decidable*if for anyT,ϕ∈𝒯T,\\phi\\in\\mathcal\{T\}, it is decidable to check ifT⊧ϕT\\models\\phi\. One popular decidable class of FO theories is thetwo\-variable fragmentwith equality, calledFO2\\textsc\{FO\}^\{2\}Grädelet al\.\([1997](https://arxiv.org/html/2605.12691#bib.bib20)\)\. It consists of all formulas with at most 2 variable symbols, which we denote asxxandyyby convention\. Byx→\\vec\{x\}we then mean a vector of variables that either consists only ofxxor ofxxandyy\.

###### Theorem 15\(Grädelet al\.\([1997](https://arxiv.org/html/2605.12691#bib.bib20)\)\)\.

FO2\\textsc\{FO\}^\{2\}has the exponential model property: there is a constantccs\.t\. every satisfiableFO2\\textsc\{FO\}^\{2\}\-sentenceϕ\\phihas a model of cardinality at most2c​\|ϕ\|2^\{c\|\\phi\|\}, where\|ϕ\|\|\\phi\|is the size ofϕ\\phi\.

Consequently, satisfiability ofFO2\\textsc\{FO\}^\{2\}is NEXPTIME\-complete and entailment checking is CoNEXPTIME\-complete\.

Typically,FO2\\textsc\{FO\}^\{2\}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 constantAA, one introduces a predicatePA​\(x\)P\_\{A\}\(x\)and includes an axiom

∃x​PA​\(x\)∧∀x​∀y\.PA​\(x\)∧PA​\(y\)⊃\(x=y\)\\exists xP\_\{A\}\(x\)\\land\\forall x\\forall y\.\\,P\_\{A\}\(x\)\\land P\_\{A\}\(y\)\\supset\(x=y\)saying that there is exactly one domain element in the extension ofPAP\_\{A\}\. It is easy to see that this idea can be extended to also include ground situation terms𝑑𝑜​\(α,S0\)\\mathit\{do\}\(\\alpha,S\_\{0\}\)\.

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 toGrädelet al\.\([1997](https://arxiv.org/html/2605.12691#bib.bib20)\)\. For fluent predicates, we allow for up to twoobjectarguments in addition to thesituationargument\. 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α\\alpha, a BAT𝒟\\mathcal\{D\}is anFO2\\textsc\{FO\}^\{2\}\-BAT wrtα\\alphaif𝒟S0∪𝒟s​s​\[α,S0\]\\mathcal\{D\}\_\{S\_\{0\}\}\\cup\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]is a finiteFO2\\textsc\{FO\}^\{2\}theory\.

In what follows, we show that the progressions ofFO2\\textsc\{FO\}^\{2\}\-BATs wrt local\-effect, normal, and acyclic actions are all within theFO2\\textsc\{FO\}^\{2\}fragment, hence decidable\.

#### FO2\\textsc\{FO\}^\{2\}\-BAT\-LE

To begin with, we considerFO2\\textsc\{FO\}^\{2\}\-BAT where the actionα\\alphahas local effects, i\.e\.,FO2\\textsc\{FO\}^\{2\}\-BAT\-LE\.

###### Theorem 17\.

Given a BAT𝒟\\mathcal\{D\}that is BAT\-LE wrt ground actionα\\alpha, if𝒟\\mathcal\{D\}is also anFO2\\textsc\{FO\}^\{2\}\-BAT wrtα\\alpha, then the progression of𝒟0\\mathcal\{D\}\_\{0\}wrt𝒟,α\\mathcal\{D\},\\alphacan be expressed inFO2\\textsc\{FO\}^\{2\}\.

It is not hard to check that\(𝒟S0∪𝒟s​s​\[Ω\]\)​\[θ\]\(\\mathcal\{D\}\_\{S\_\{0\}\}\\cup\\mathcal\{D\}\_\{ss\}\[\\Omega\]\)\[\\theta\]in Eq\. \([4](https://arxiv.org/html/2605.12691#S3.E4)\) is inFO2\\textsc\{FO\}^\{2\}by assumption\. Besides, a disjunction ofFO2\\textsc\{FO\}^\{2\}theories is still inFO2\\textsc\{FO\}^\{2\}, so the progression as in Eq\. \([4](https://arxiv.org/html/2605.12691#S3.E4)\) is inFO2\\textsc\{FO\}^\{2\}\.

#### FO2\\textsc\{FO\}^\{2\}\-BAT\-NR

ForFO2\\textsc\{FO\}^\{2\}\-BAT with normal actions, we have

###### Theorem 18\.

Given a BAT𝒟\\mathcal\{D\}that is BAT\-NR wrt ground actionα\\alpha, if𝒟\\mathcal\{D\}is anFO2\\textsc\{FO\}^\{2\}\-BAT wrtα\\alpha, then the progression of𝒟0\\mathcal\{D\}\_\{0\}wrt𝒟,α\\mathcal\{D\},\\alphacan be expressed inFO2\\textsc\{FO\}^\{2\}\.

For BAT\-NR, forgetting NLE fluents as in Thm\.[5](https://arxiv.org/html/2605.12691#Thmtheorem5)involves combining sufficient conditions and necessary conditions of semi\-definitional formulas, which clearly does not introduce new variables\. Hence, the result is still inFO2\\textsc\{FO\}^\{2\}\. Besides, for LE fluents, as mentioned before, forgetting them only involves disjoining twoFO2\\textsc\{FO\}^\{2\}theories, which is still inFO2\\textsc\{FO\}^\{2\}\. Hence, the resulting progression is inFO2\\textsc\{FO\}^\{2\}\.

#### FO2\\textsc\{FO\}^\{2\}\-BAT\-AC

The situation forFO2\\textsc\{FO\}^\{2\}\-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 inFO2\\textsc\{FO\}^\{2\}\. The following lemma justifies this\.

###### Lemma 19\.

Ifϕ​\(x→\)∈FO2\\phi\(\\vec\{x\}\)\\in\\textsc\{FO\}^\{2\}is in good form wrtPP, then

1. 1\.ϕ​\(x→\)\\phi\(\\vec\{x\}\)can be rewritten to a formula inFO2\\textsc\{FO\}^\{2\}that is semi\-definitional wrtPP;
2. 2\.¬ϕ​\(x→\)\\neg\\phi\(\\vec\{x\}\)can be rewritten to a formula inFO2\\textsc\{FO\}^\{2\}that is in good form wrtPP\.

The proof of Item 2 is simple, as the rewrite only involves pushing negation inward and distributing conjunctions over disjunctions, operations that preserve membership inFO2\\textsc\{FO\}^\{2\}\. For Item 1, letϕ​\(x→\)=\{∀x→​\(ψ​\(x→\)∨P​\(t→\)\),∀x→​\(ψ′​\(x→\)∨¬P​\(t→\)\),∀x→​ψ′′​\(x→\)\}\\phi\(\\vec\{x\}\)=\\\{\\forall\\vec\{x\}\(\\psi\(\\vec\{x\}\)\\vee P\(\\vec\{t\}\)\),\\forall\\vec\{x\}\(\\psi^\{\\prime\}\(\\vec\{x\}\)\\vee\\neg P\(\\vec\{t\}\)\),\\forall\\vec\{x\}\\psi^\{\\prime\\prime\}\(\\vec\{x\}\)\\\}\. By assumption,x→\\vec\{x\}denotes either onlyxxorxxandyy\. SincePPis unary or binary,t→\\vec\{t\}has length one or two, and since functions are excluded,t→\\vec\{t\}can only consist of a combination ofxx,yy, and some constantsAAandBB\. Hence, for∀x→​\(ψ​\(x→\)∨P​\(t→\)\)\\forall\\vec\{x\}\(\\psi\(\\vec\{x\}\)\\vee P\(\\vec\{t\}\)\)\(likewise for the¬P\\neg Pcase\), we have cases:

- •∀x​\(ψ​\(x\)∨P​\(A\)\)⇔∀x​\(\(x=A\)∧∃x​¬ψ​\(x\)\)⊃P​\(x\)\\forall x\(\\psi\(x\)\\lor P\(A\)\)\\Leftrightarrow\\forall x\(\(x=A\)\\land\\exists x\\lnot\\psi\(x\)\)\\supset P\(x\)\.
- •∀x​\(ψ​\(x\)∨P​\(x\)\)\\forall x\(\\psi\(x\)\\lor P\(x\)\)has the right form already\.
- •∀x​∀y​\(ψ​\(x,y\)∨P​\(A,B\)\)\\forall x\\forall y\(\\psi\(x,y\)\\lor P\(A,B\)\)can be rewritten as ∀x​∀y​\(\(x=A∧y=B\)∧∃x​∃y​¬ψ​\(x,y\)\)⊃P​\(x,y\)\\forall x\\forall y\(\(x=A\\land y=B\)\\land\\exists x\\exists y\\lnot\\psi\(x,y\)\)\\supset P\(x,y\)\.
- •∀x​∀y​\(ψ​\(x,y\)∨P​\(x,B\)\)\\forall x\\forall y\(\\psi\(x,y\)\\lor P\(x,B\)\)can be rewritten as ∀x​∀y​\(\(y=B\)∧∃y​¬ψ​\(x,y\)\)⊃P​\(x,y\)\\forall x\\forall y\(\(y=B\)\\land\\exists y\\lnot\\psi\(x,y\)\)\\supset P\(x,y\)\.
- •∀x​∀y​\(ψ​\(x,y\)∨P​\(A,y\)\)\\forall x\\forall y\(\\psi\(x,y\)\\lor P\(A,y\)\)can be rewritten as ∀x​∀y​\(\(x=A\)∧∃x​¬ψ​\(x,y\)\)⊃P​\(x,y\)\\forall x\\forall y\(\(x=A\)\\land\\exists x\\lnot\\psi\(x,y\)\)\\supset P\(x,y\)\.
- •∀x​∀y​\(ψ​\(x,y\)∨P​\(x,y\)\)\\forall x\\forall y\(\\psi\(x,y\)\\lor P\(x,y\)\)has the right form already\.

Hence∀x→​\(ψ​\(x→\)∨P​\(t→\)\)\\forall\\vec\{x\}\(\\psi\(\\vec\{x\}\)\\vee P\(\\vec\{t\}\)\), thusϕ​\(x→\)\\phi\(\\vec\{x\}\), can be expressed inFO2\\textsc\{FO\}^\{2\}\.

###### Theorem 20\.

Given a BAT𝒟\\mathcal\{D\}that is BAT\-AC wrt ground actionα\\alpha, if𝒟\\mathcal\{D\}is aFO2\\textsc\{FO\}^\{2\}\-BAT wrtα\\alpha, then the progression of𝒟0\\mathcal\{D\}\_\{0\}wrt𝒟,α\\mathcal\{D\},\\alphacan be expressed inFO2\\textsc\{FO\}^\{2\}\.

We remark that the results in this section are not obvious in the following sense\.FO2\\textsc\{FO\}^\{2\}is a fragment that fails to have the Craig interpolation and Beth definability propertiesJung and Wolter \([2021](https://arxiv.org/html/2605.12691#bib.bib15)\)\. Among other things, this means that while forgetting a predicatePPfrom aFO2\\textsc\{FO\}^\{2\}theory might be possible \(i\.e\., yields an equivalent FO theory\), it can happen that the resulting theory is not expressible inFO2\\textsc\{FO\}^\{2\}\. Hence, not everyFO2\\textsc\{FO\}^\{2\}\-BAT has a progression that is inFO2\\textsc\{FO\}^\{2\}, but for the fragments we consider here, this can be guaranteed\.

## 5Universal Theories with Constants

Another decidable fragment of FOL is given by universal theories with constants \(UTC\)\. In fact, it is shown that Bernays\-SchönfinkelBernays and Schönfinkel \([1928](https://arxiv.org/html/2605.12691#bib.bib25)\)\(BS\) theories are decidable, i\.e\., theories with sentences of the form∃x1​…​∃xk​∀y1​⋯​∀ym​ϕ\\exists x\_\{1\}\\ldots\\exists x\_\{k\}\\forall y\_\{1\}\\cdots\\forall y\_\{m\}\\phi, whereϕ\\phiis 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​ϕ\\forall y\_\{1\}\\cdots\\forall y\_\{m\}\\phi\. ForUTCtheoryTTand queryϕ\\phi, deciding ifT⊧ϕT\\models\\phican be converted to check if the BS theoryT∪\{¬ϕ\}T\\cup\\\{\\neg\\phi\\\}is unsatisfiable, hence the complexity is CoNEXPTIME\-complete\.

###### Definition 21\.

Given a ground actionα\\alpha, a BAT𝒟\\mathcal\{D\}is aUTC\-BAT wrtα\\alphaif𝒟S0∪𝒟s​s​\[α,S0\]\\mathcal\{D\}\_\{S\_\{0\}\}\\cup\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]is a finiteUTCtheory\.

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

#### UTC\-BAT\-LE

First, for local effect actions, we have that

###### Theorem 22\.

Given a BAT𝒟\\mathcal\{D\}that is BAT\-LE wrt ground actionα\\alpha, if𝒟\\mathcal\{D\}is anUTC\-BAT wrtα\\alpha, then the progression of𝒟0\\mathcal\{D\}\_\{0\}wrt𝒟,α\\mathcal\{D\},\\alphacan be expressed inUTC\.

Again, the key here is to show that the disjunction of UTC theories can be expressed inUTC\. This is indeed the case by applying the following rule to properly rename variables∀x→​ϕ​\(x→\)∨∀x→​ψ​\(x→\)⇔∀x→​∀y→​\(ϕ​\(x→\)∨ψ​\(y→\)\)\\forall\\vec\{x\}\\phi\(\\vec\{x\}\)\\vee\\forall\\vec\{x\}\\psi\(\\vec\{x\}\)\\Leftrightarrow\\forall\\vec\{x\}\\forall\\vec\{y\}\(\\phi\(\\vec\{x\}\)\\vee\\psi\(\\vec\{y\}\)\)\.

#### UTC\-BAT\-NR

Likewise, for normal actions, we have

###### Theorem 23\.

Given a BAT𝒟\\mathcal\{D\}that is BAT\-NR wrt ground actionα\\alpha, if𝒟\\mathcal\{D\}is anUTC\-BAT wrtα\\alpha, then the progression of𝒟0\\mathcal\{D\}\_\{0\}wrt𝒟,α\\mathcal\{D\},\\alphacan be expressed inUTC\.

The proof is like its counterpart inFO2\\textsc\{FO\}^\{2\}, it suffices to show that forgetting NLE fluents preserves membership inUTC\. This is indeed the case as the sufficient and necessary conditions to be combined when forgetting NLE fluents, as in Thm\.[5](https://arxiv.org/html/2605.12691#Thmtheorem5), are all quantifier\-free by assumption; hence, the result is still quantifier\-free, leading to aUTCFO progression\.

#### UTC\-BAT\-AC

Lastly, for acyclic actions, we have that

###### Lemma 24\.

Ifϕ​\(x→\)∈UTC\\phi\(\\vec\{x\}\)\\in\\textsc\{UTC\}is in good form wrtPP, then

1. 1\.ϕ​\(x→\)\\phi\(\\vec\{x\}\)can be rewritten to a formula inUTCthat is semi\-definitional wrtPP;
2. 2\.¬ϕ​\(x→\)\\neg\\phi\(\\vec\{x\}\)can be rewritten to a formula inUTCthat is in good form wrtPP\.

Again, Item 2 is trivial as the rewrite only involves pushing negation inward and distributing conjunctions over disjunctions, operations that preserve membership inUTC\. We prove the first item\. For Item 1, letϕ​\(x→\)=\{∀x→​\(ψ​\(x→\)∨P​\(t→\)\),∀x→​\(ψ′​\(x→\)∨¬P​\(t→\)\),∀x→​ψ′′​\(x→\)\}\\phi\(\\vec\{x\}\)=\\\{\\forall\\vec\{x\}\(\\psi\(\\vec\{x\}\)\\vee P\(\\vec\{t\}\)\),\\forall\\vec\{x\}\(\\psi^\{\\prime\}\(\\vec\{x\}\)\\vee\\neg P\(\\vec\{t\}\)\),\\forall\\vec\{x\}\\psi^\{\\prime\\prime\}\(\\vec\{x\}\)\\\}\.ψ​\(x→\),ψ′​\(x→\),ψ′′​\(x→\)\\psi\(\\vec\{x\}\),\\psi^\{\\prime\}\(\\vec\{x\}\),\\psi^\{\\prime\\prime\}\(\\vec\{x\}\)are all quantifier\-free andt→\\vec\{t\}can only contain variables inx→\\vec\{x\}by assumption\.∀x→​\(ψ​\(x→\)∨P​\(t→\)\)\\forall\\vec\{x\}\(\\psi\(\\vec\{x\}\)\\vee P\(\\vec\{t\}\)\)\(likewise for the¬P\\neg Pcase\) can be rewritten as∀x→​∀y→\.y→=t→⊃\(ψ​\(x→\)∨P​\(y→\)\)\\forall\\vec\{x\}\\forall\\vec\{y\}\.\\vec\{y\}=\\vec\{t\}\\supset\(\\psi\(\\vec\{x\}\)\\vee P\(\\vec\{y\}\)\), which is in UTC and semi\-definitional wrtPP, and hence so canϕ​\(x\)\\phi\(x\)\.

###### Theorem 25\.

Given a BAT𝒟\\mathcal\{D\}that is BAT\-AC wrt ground actionα\\alpha, if𝒟\\mathcal\{D\}is anUTC\-BAT wrtα\\alpha, then the progression of𝒟0\\mathcal\{D\}\_\{0\}wrt𝒟,α\\mathcal\{D\},\\alphacan be expressed inUTC\.

We remark that the fact that the progression of a UTC\-BAT can be expressed by another UTC theory here is not so surprising, asArenaset al\.\([2018](https://arxiv.org/html/2605.12691#bib.bib5)\)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 UTC\-BATs actually exist \(and can be computed accordingly\)\. In addition, due to our results in Section[3](https://arxiv.org/html/2605.12691#S3), the size of such finite progressions grows only polynomially, even linearly\.

## 6Related Work 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 LakemeyerLiu and Lakemeyer \([2009](https://arxiv.org/html/2605.12691#bib.bib2)\)and due to Liu and ClaßenLiu and Claßen \([2024](https://arxiv.org/html/2605.12691#bib.bib6)\), 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\-calledproper\+\\textrm\{proper\}^\{\+\}form\. Intuitively,proper\+\\textrm\{proper\}^\{\+\}KBsLakemeyer and Levesque \([2002](https://arxiv.org/html/2605.12691#bib.bib9)\)correspond to consistent, potentially infinite sets of ground clauses\. What makes them particularly interesting is that certain queries can be computed in polynomial timeLiu and Levesque \([2005](https://arxiv.org/html/2605.12691#bib.bib10)\)\. De Giacomo et al\.De Giacomoet al\.\([2016](https://arxiv.org/html/2605.12691#bib.bib22)\)showed that progression is FO definable for Situation Calculus theories where the number of fluent instances affected by an action isbounded, in which case verification \(and hence projection\) is decidable\. Arenas et al\.Arenaset al\.\([2018](https://arxiv.org/html/2605.12691#bib.bib5)\)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àEiter and Soldà \([2024](https://arxiv.org/html/2605.12691#bib.bib8)\)studied computational aspects of progression in the context of temporal equilibrium logic\.

More broadly, related work includes that by Gu and SoutchanskiGu and Soutchanski \([2010](https://arxiv.org/html/2605.12691#bib.bib21)\)who studied the complexity ofregressionfor action theories over the two\-variable fragment of FOL with counting quantifiers as well as description logics𝒜​ℒ​𝒞​𝒪​\(U\)\{\\cal ALCO\}\(U\)and𝒜​ℒ​𝒞​𝒬​𝒪​\(U\)\{\\cal ALCQO\}\(U\)\. Lakemeyer and LevesqueLakemeyer and Levesque \([2014](https://arxiv.org/html/2605.12691#bib.bib11)\)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\.Calvaneseet al\.\([2015](https://arxiv.org/html/2605.12691#bib.bib12)\)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ßZarrieß \([2018](https://arxiv.org/html/2605.12691#bib.bib26)\)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 ofFO2\\textsc\{FO\}^\{2\}, related results on projection are not directly applicable to aFO2\\textsc\{FO\}^\{2\}\-based Situation Calculus since translatingFO2\\textsc\{FO\}^\{2\}into description logic leads to a \(provably unavoidable\) exponential blow\-upLutzet al\.\([2001](https://arxiv.org/html/2605.12691#bib.bib14)\)\.

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 inZarrieß and Claßen \([2016](https://arxiv.org/html/2605.12691#bib.bib4)\)\. 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 representationsCorrêa and De Giacomo \([2024](https://arxiv.org/html/2605.12691#bib.bib13)\), 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\.

## Appendix

### Proof of Theorem[13](https://arxiv.org/html/2605.12691#Thmtheorem13)

First, we provide a detailed proof for Proposition[12](https://arxiv.org/html/2605.12691#Thmtheorem12)\.

###### Proposition\(Restatement of Proposition[12](https://arxiv.org/html/2605.12691#Thmtheorem12)\)\.

Ifϕ​\(x→\)\\phi\(\\vec\{x\}\)is in good form wrtPP, then

1. 1\.ϕ​\(x→\)\\phi\(\\vec\{x\}\)can be rewritten toφ​\(y→\)\\varphi\(\\vec\{y\}\)that is semi\-definitional wrtP​\(y→\)P\(\\vec\{y\}\), moreover, ifa=max⁡\{\|x→\|,\|y→\|\}a=\\max\\\{\|\\vec\{x\}\|,\|\\vec\{y\}\|\\\}, then\|φ​\(y→\)\|≤\|ϕ​\(x→\)\|\+7​a\+2\|\\varphi\(\\vec\{y\}\)\|\\leq\|\\phi\(\\vec\{x\}\)\|\+7a\+2and\|φ​\(y→\)\|P≤\|ϕ​\(x→\)\|P\+3​a\+1\|\\varphi\(\\vec\{y\}\)\|\_\{P\}\\leq\|\\phi\(\\vec\{x\}\)\|\_\{P\}\+3a\+1;
2. 2\.¬ϕ​\(x→\)\\lnot\\phi\(\\vec\{x\}\)can be rewritten toφ​\(x→\)\\varphi\(\\vec\{x\}\)that is in good form wrtPPwith\|φ​\(x→\)\|≤3​\|ϕ​\(x→\)\|\|\\varphi\(\\vec\{x\}\)\|\\leq 3\|\\phi\(\\vec\{x\}\)\|and\|φ​\(x→\)\|P≤3​\|ϕ​\(x→\)\|P\+2\|\\varphi\(\\vec\{x\}\)\|\_\{P\}\\leq 3\|\\phi\(\\vec\{x\}\)\|\_\{P\}\+2;
3. 3\.ifψ​\(x→\)\\psi\(\\vec\{x\}\)mentions noPP, thenϕ​\(x→\)∨ψ​\(x→\)\\phi\(\\vec\{x\}\)\\lor\\psi\(\\vec\{x\}\)can be rewritten to a formulaφ​\(x→\)\\varphi\(\\vec\{x\}\)in good form wrtPP, where\|φ​\(x→\)\|=\|ϕ​\(x→\)\|\+3​\|ψ​\(x→\)\|\+3\|\\varphi\(\\vec\{x\}\)\|=\|\\phi\(\\vec\{x\}\)\|\+3\|\\psi\(\\vec\{x\}\)\|\+3and\|φ​\(x→\)\|P=\|ϕ​\(x→\)\|P\+\|ψ​\(x→\)\|\+1\|\\varphi\(\\vec\{x\}\)\|\_\{P\}=\|\\phi\(\\vec\{x\}\)\|\_\{P\}\+\|\\psi\(\\vec\{x\}\)\|\+1\.

###### Proof\.

Letϕ​\(x→\)=\(ψ​\(x→\)∨P​\(t→\)\)∧\(ψ′​\(x→\)∨¬P​\(t→\)\)∧ψ′′​\(x→\)\\phi\(\\vec\{x\}\)=\(\\psi\(\\vec\{x\}\)\\lor P\(\\vec\{t\}\)\)\\land\(\\psi^\{\\prime\}\(\\vec\{x\}\)\\lor\\lnot P\(\\vec\{t\}\)\)\\land\\psi^\{\\prime\\prime\}\(\\vec\{x\}\),

1. 1\.ϕ​\(x→\)\\phi\(\\vec\{x\}\)is equivalent toφ​\(y→\)\\varphi\(\\vec\{y\}\)given by \(\(∀x→\.y→≠t→∨ψ\(x→\)\)∨P\(y→\)\)∧\\displaystyle\(\(\\forall\\vec\{x\}\.\\,\\vec\{y\}\\neq\\vec\{t\}\\lor\\psi\(\\vec\{x\}\)\)\\lor P\(\\vec\{y\}\)\)~\\land\(9\)\(\(∀x→\.y→≠t→∨ψ′\(x→\)\)∨¬P\(y→\)\)∧\(∀x→\.ψ′′\(x→\)\)\\displaystyle\(\(\\forall\\vec\{x\}\.\\,\\vec\{y\}\\neq\\vec\{t\}\\lor\\psi^\{\\prime\}\(\\vec\{x\}\)\)\\lor\\lnot P\(\\vec\{y\}\)\)~\\land~\(\\forall\\vec\{x\}\.\\,\\psi^\{\\prime\\prime\}\(\\vec\{x\}\)\)Hence, the size increases by 3 occurrences of∀x→\\forall\\vec\{x\}\(each sizell\), 2 occurrences of\(y→≠t→\)\(\\vec\{y\}\\neq\\vec\{t\}\)\(each size 2ll\), and two additional disjunction symbols;
2. 2\.¬ϕ​\(x→\)\\lnot\\phi\(\\vec\{x\}\)is equivalent to a formulaφ​\(x→\)\\varphi\(\\vec\{x\}\)given by \(¬ψ​\(x→\)∨¬ψ′′​\(x→\)∨P​\(t→\)\)∧\(¬ψ′​\(x→\)∨¬ψ′′​\(x→\)∨¬P​\(t→\)\)∧\(¬ψ​\(x→\)∨¬ψ′​\(x→\)∨¬ψ′′​\(x→\)\)\(\\lnot\\psi\(\\vec\{x\}\)\\lor\\lnot\\psi^\{\\prime\\prime\}\(\\vec\{x\}\)\\lor P\(\\vec\{t\}\)\)~\\land\(\\lnot\\psi^\{\\prime\}\(\\vec\{x\}\)\\lor\\lnot\\psi^\{\\prime\\prime\}\(\\vec\{x\}\)\\lor\\lnot P\(\\vec\{t\}\)\)~\\land\(\\lnot\\psi\(\\vec\{x\}\)\\lor\\lnot\\psi^\{\\prime\}\(\\vec\{x\}\)\\lor\\lnot\\psi^\{\\prime\\prime\}\(\\vec\{x\}\)\) Letl1=\|ψ​\(x→\)\|l\_\{1\}=\|\\psi\(\\vec\{x\}\)\|,l2=\|ψ′​\(x→\)\|l\_\{2\}=\|\\psi^\{\\prime\}\(\\vec\{x\}\)\|, andl3=\|ψ′′​\(x→\)\|l\_\{3\}=\|\\psi^\{\\prime\\prime\}\(\\vec\{x\}\)\|\. Then\|ϕ​\(x→\)\|=l1\+l2\+l3\+7\|\\phi\(\\vec\{x\}\)\|=l\_\{1\}\+l\_\{2\}\+l\_\{3\}\+7, and\|φ​\(x→\)\|=2​l1\+2​l2\+3​l3\+18\|\\varphi\(\\vec\{x\}\)\|=2l\_\{1\}\+2l\_\{2\}\+3l\_\{3\}\+18\. Also,\|ϕ​\(x→\)\|P=max⁡\{l1,l2,l3\}\|\\phi\(\\vec\{x\}\)\|\_\{P\}=\\max\\\{l\_\{1\},l\_\{2\},l\_\{3\}\\\}, and every condition inφ​\(x→\)\\varphi\(\\vec\{x\}\)has size≤l1\+l2\+l3\+2≤\|φ​\(x→\)\|P\+2\\leq l\_\{1\}\+l\_\{2\}\+l\_\{3\}\+2\\leq\|\\varphi\(\\vec\{x\}\)\|\_\{P\}\+2;
3. 3\.ϕ​\(x→\)∨ψ​\(x→\)\\phi\(\\vec\{x\}\)\\lor\\psi\(\\vec\{x\}\)is equivalent toφ​\(x→\)\\varphi\(\\vec\{x\}\)given by \(ψ​\(x→\)∨ψ′​\(x→\)∨P​\(t→\)\)∧\(ψ​\(x→\)∨ψ′′​\(x→\)∨¬P​\(t→\)\)∧\(ψ​\(x→\)∨ψ′′′​\(x→\)\)\(\\psi\(\\vec\{x\}\)\\lor\\psi^\{\\prime\}\(\\vec\{x\}\)\\lor P\(\\vec\{t\}\)\)~\\land\(\\psi\(\\vec\{x\}\)\\lor\\psi^\{\\prime\\prime\}\(\\vec\{x\}\)\\lor\\lnot P\(\\vec\{t\}\)\)~\\land\(\\psi\(\\vec\{x\}\)\\lor\\psi^\{\\prime\\prime\\prime\}\(\\vec\{x\}\)\)\. Observe that the new formula adds 3 occurrences ofψ​\(x→\)\\psi\(\\vec\{x\}\)and 3 disjunction symbols toϕ​\(x→\)\\phi\(\\vec\{x\}\)\.

∎

###### Theorem\(Restatement of Theorem[13](https://arxiv.org/html/2605.12691#Thmtheorem13)\)\.

If𝒟\\mathcal\{D\}is BAT\-AC wrt ground actionα\\alpha, the result of forgetting the lifting predicates for all fluents inNLE​\(α\)\\mathrm\{NLE\}\(\\alpha\)in\(𝒟S0∪𝒟s​s​\[α,S0\]\)↑S0\(\\mathcal\{D\}\_\{S\_\{0\}\}\\cup\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]\)\\uparrow S\_\{0\}can be represented by a FO theory whose size is inO​\(2d​\(n\+m\)\)O\(2^\{d\}\(n\+m\)\), whereddis the depth of the dependency graph,nnthe size of𝒟S0\\mathcal\{D\}\_\{S\_\{0\}\}, andmmthe size of𝒟s​s\\mathcal\{D\}\_\{ss\}\.

###### Proof\.

The proof for Theorem 3 inLiu and Claßen \([2024](https://arxiv.org/html/2605.12691#bib.bib6)\)makes an inductive argument that it is possible to iteratively forget fluents inNLE​\(α\)\\mathrm\{NLE\}\(\\alpha\)of decreasing fluent depth while maintaining the required form\. Looking at an arbitraryFF, this means that we forget all its predecessorsF∗F^\{\*\}before forgettingFFitself\. By induction assumption, none of theF∗F^\{\*\}have any predecessors to consider, and there is a single semi\-definitional axiom of the form

ΔF=\(𝑁𝑊𝑆F​\(x→\)∨F​\(x→,S0\)\)∧\(𝑆𝑁𝐶F​\(x→\)∨¬F​\(x→,S0\)\)\\displaystyle\\Delta\_\{F\}=\\left\(\\mathit\{NWS\}\_\{F\}\(\\vec\{x\}\)\\lor F\(\\vec\{x\},S\_\{0\}\)\\right\)\\land\\left\(\\mathit\{SNC\}\_\{F\}\(\\vec\{x\}\)\\lor\\lnot F\(\\vec\{x\},S\_\{0\}\)\\right\)in the initial KB for each of them \(letΔF\\Delta\_\{F\}denote the axiom forFFhenceforth\)\. Hence, to forgetFF, one only needs to considerΔF∧𝒟s​sF​\[α,S0\]\\Delta\_\{F\}\\land\\mathcal\{D\}^\{F\}\_\{ss\}\[\\alpha,S\_\{0\}\], which by Prop\. 6 amounts to replacing the originalΔF\\Delta\_\{F\}by the following \(parameters ofγF±\\gamma^\{\\pm\}\_\{F\}are omitted, expressions in parentheses are explained further below\):

𝑁𝑊𝑆F​\(x→\)∨𝑆𝑁𝐶F​\(x→\)\\displaystyle\\mathit\{NWS\}\_\{F\}\(\\vec\{x\}\)\\lor\\mathit\{SNC\}\_\{F\}\(\\vec\{x\}\)\([7a](https://arxiv.org/html/2605.12691#S3.E7.1)\)¬γF\+∨F​\(x→,Sα\)\\displaystyle\\lnot\\gamma\_\{F\}^\{\+\}\\lor F\(\\vec\{x\},S\_\{\\alpha\}\)\(3​k\+4\)\\displaystyle\(3k\+4\)\([7b](https://arxiv.org/html/2605.12691#S3.E7.2)\)¬γF−∨¬F​\(x→,Sα\)\\displaystyle\\lnot\\gamma\_\{F\}^\{\-\}\\lor\\lnot F\(\\vec\{x\},S\_\{\\alpha\}\)\(3​k\+5\)\\displaystyle\(3k\+5\)\([7c](https://arxiv.org/html/2605.12691#S3.E7.3)\)γF\+∨¬F​\(x→,Sα\)∨𝑆𝑁𝐶F​\(x→\)\\displaystyle\\gamma\_\{F\}^\{\+\}\\lor\\lnot F\(\\vec\{x\},S\_\{\\alpha\}\)\\lor\\mathit\{SNC\}\_\{F\}\(\\vec\{x\}\)\(wF\+k\+4\)\\displaystyle\(w\_\{F\}\+k\+4\)\([7d](https://arxiv.org/html/2605.12691#S3.E7.4)\)𝑁𝑊𝑆F​\(x→\)∨γF−∨F​\(x→,Sα\)\\displaystyle\\mathit\{NWS\}\_\{F\}\(\\vec\{x\}\)\\lor\\gamma\_\{F\}^\{\-\}\\lor F\(\\vec\{x\},S\_\{\\alpha\}\)\(wF\+k\+3\)\\displaystyle\(w\_\{F\}\+k\+3\)\([7e](https://arxiv.org/html/2605.12691#S3.E7.5)\)Formula \([7a](https://arxiv.org/html/2605.12691#S3.E7.1)\) will remain unchanged when forgetting subsequent fluents \(recall that𝑁𝑊𝑆F\\mathit\{NWS\}\_\{F\}and𝑆𝑁𝐶F\\mathit\{SNC\}\_\{F\}do not mention any NLE fluents\)\. By definition, there are at most two other NLE fluentsF\+′,F−′F^\{\\prime\}\_\{\+\},F^\{\\prime\}\_\{\-\}in the dependency graph such thatF→F\+′F\\rightarrow F^\{\\prime\}\_\{\+\}andF→F−′F\\rightarrow F^\{\\prime\}\_\{\-\}, whereF\+′F^\{\\prime\}\_\{\+\}only occurs inγF\+\\gamma\_\{F\}^\{\+\}, andF−′F^\{\\prime\}\_\{\-\}only inγF−\\gamma\_\{F\}^\{\-\}\. Formulas \([7b](https://arxiv.org/html/2605.12691#S3.E7.2)\) and \([7d](https://arxiv.org/html/2605.12691#S3.E7.4)\) will subsequently be incorporated into the new KB axiomΔF\+′\\Delta\_\{F^\{\\prime\}\_\{\+\}\}, and formulas \([7a](https://arxiv.org/html/2605.12691#S3.E7.1)\) and \([7e](https://arxiv.org/html/2605.12691#S3.E7.5)\) into the new axiomΔF−′\\Delta\_\{F^\{\\prime\}\_\{\-\}\}\.

We now estimate the condition size ofΔF′\\Delta\_\{F^\{\\prime\}\}in terms of the conditions size ofΔF\\Delta\_\{F\}forF→F′F\\rightarrow F^\{\\prime\}\. For this purpose, letwFw\_\{F\}denote the condition size of theupdatedΔF\\Delta\_\{F\}for anyFF, after its predecessors have been forgotten, but before forgettingFFitself\. Furthermore, letkkbe the maximal size of an SSA for any NLE fluent, andwwbe the maximal condition size of anyΔF\\Delta\_\{F\}in the original KB\. Using Prop\.[12](https://arxiv.org/html/2605.12691#Thmtheorem12), this gives us upper bounds for the condition sizes of formulas \([7b](https://arxiv.org/html/2605.12691#S3.E7.2)\)–\([7e](https://arxiv.org/html/2605.12691#S3.E7.5)\) as stated above in parentheses\. Observe that the sum of condition sizes of \([7b](https://arxiv.org/html/2605.12691#S3.E7.2)\) and \([7d](https://arxiv.org/html/2605.12691#S3.E7.4)\) forF\+′F^\{\\prime\}\_\{\+\}is the same as the sum of condition sizes for \([7c](https://arxiv.org/html/2605.12691#S3.E7.3)\) and \([7e](https://arxiv.org/html/2605.12691#S3.E7.5)\) forF−′F^\{\\prime\}\_\{\-\}, namelywF\+4​k\+8w\_\{F\}\+4k\+8\. Also by Prop\.[12](https://arxiv.org/html/2605.12691#Thmtheorem12), converting each of them to semi\-definitional form adds at most\(3​a\+1\)\(3a\+1\)to their individual condition size, whereaais the maximal arity among all fluents\. The originalΔF′\\Delta\_\{F^\{\\prime\}\}already have the right form, and their condition size is bounded byww\. Putting these together, by Prop\.[11](https://arxiv.org/html/2605.12691#Thmtheorem11)we have that the condition size for the updatedΔF′\\Delta\_\{F^\{\\prime\}\}is bounded according to

wF′\\displaystyle w\_\{F^\{\\prime\}\}≤w\+∑F→F′\(wF\+4​k\+6​a\+10\)\.\\displaystyle\\leq w\+\\sum\_\{F\\rightarrow F^\{\\prime\}\}\(w\_\{F\}\+4k\+6a\+10\)\.\([8](https://arxiv.org/html/2605.12691#S3.E8)\)Note that this bound also holds for fluents without predecessors in the dependency graph; in this case, the sum is empty and onlywwremains\.

For determining the size of the resulting KB, note that formulas of the form \([7a](https://arxiv.org/html/2605.12691#S3.E7.1)\) are added for all NLE fluents\. Formulas of the form \([7c](https://arxiv.org/html/2605.12691#S3.E7.3)\)–\([7e](https://arxiv.org/html/2605.12691#S3.E7.5)\) are deleted in case that theγF±\\gamma\_\{F\}^\{\\pm\}mention other NLE fluentsF′F^\{\\prime\}, but kept if they only mention LE fluents\. An upper bound is hence given by the sum of sizes of \([7a](https://arxiv.org/html/2605.12691#S3.E7.1)\)–\([7e](https://arxiv.org/html/2605.12691#S3.E7.5)\) overallNLE fluentsFF\. Observe that the total size of occurrences ofγF±\\gamma\_\{F\}^\{\\pm\},F​\(x→,Sα\)F\(\\vec\{x\},S\_\{\\alpha\}\)atoms, and boolean connectives is less than the size of𝒟s​sF​\[α,S0\]\\mathcal\{D\}\_\{ss\}^\{F\}\[\\alpha,S\_\{0\}\]when using the representation of Prop\. 6, summing up to less than\|𝒟s​s​\[α,S0\]\|\|\\mathcal\{D\}\_\{ss\}\[\\alpha,S\_\{0\}\]\|over all NLE fluents\. This leaves two occurrences of𝑁𝑊𝑆F​\(x→\)\\mathit\{NWS\}\_\{F\}\(\\vec\{x\}\)and two occurrences of𝑆𝑁𝐶F​\(x→\)\\mathit\{SNC\}\_\{F\}\(\\vec\{x\}\), each of size≤wF\\leq w\_\{F\}, summing up to

S=4​∑F∈NLE​\(α\)wF\.\\displaystyle S=4\\sum\_\{F\\in\\mathrm\{NLE\}\(\\alpha\)\}w\_\{F\}\.To determine the sum of allwFw\_\{F\}, we use the intuition that the linear recurrence in \([8](https://arxiv.org/html/2605.12691#S3.E8)\) can be unrolled along all source\-to\-node paths\. Intuitively, each node starts with awFw\_\{F\}“weight” ofww\. For each child, a nodeFFaddswF\+4​k\+6​a\+10w\_\{F\}\+4k\+6a\+10to each of its children\. This contribution ofFFis added multiple times, namely for each path starting inFF\. Because the out\-degree is bounded by 2, the number of distinct paths starting inFFis≤2d\+1\\leq 2^\{d\+1\}, whereddis the depth of the dependency graph\. If the number of NLE fluents isll, we hence getS≤4⋅2d\+1⋅l⋅\(w\+4​k\+6​a\+10\)S\\leq 4\\cdot 2^\{d\+1\}\\cdot l\\cdot\(w\+4k\+6a\+10\)\. The claim follows from the facts thataais a constant,l⋅w∈O​\(\|𝒟S0\|\)l\\cdot w\\in O\(\|\\mathcal\{D\}\_\{S\_\{0\}\}\|\), andl⋅k∈O​\(\|𝒟s​s\|\)l\\cdot k\\in O\(\|\\mathcal\{D\}\_\{ss\}\|\)\. ∎

### Proof of Theorem[18](https://arxiv.org/html/2605.12691#Thmtheorem18)

To prove Theorem[18](https://arxiv.org/html/2605.12691#Thmtheorem18), we need the following lemma\.

###### Lemma 26\.

IfTTis anFO2\\textsc\{FO\}^\{2\}theory and semi\-definitional wrtPP, then𝑓𝑜𝑟𝑔𝑒𝑡​\(T,P\)\\mathit\{forget\}\(T,P\)can be expressed inFO2\\textsc\{FO\}^\{2\}\.

The proof is directly by Thm\. 5\.𝑓𝑜𝑟𝑔𝑒𝑡​\(T,P\)\\mathit\{forget\}\(T,P\)⇔\\LeftrightarrowT′∧⋀ψ∈WSCP,ϕ∈SNCP∀x→\.ψ​\(x→\)⊃ϕ​\(x→\)T^\{\\prime\}\\land\\bigwedge\_\{\\psi\\in\\mathrm\{WSC\}\_\{P\},\\phi\\in\\mathrm\{SNC\}\_\{P\}\}\\forall\\vec\{x\}\.\\psi\(\\vec\{x\}\)\\supset\\phi\(\\vec\{x\}\)\. SinceT′T^\{\\prime\},ψ\\psi, andϕ\\phican mention at most two variablesx,yx,y,𝑓𝑜𝑟𝑔𝑒𝑡​\(T,P\)∈FO2\\mathit\{forget\}\(T,P\)\\in\\textsc\{FO\}^\{2\}\.

###### Theorem\(Restatement of Theorem[18](https://arxiv.org/html/2605.12691#Thmtheorem18)\)\.

Given a BAT𝒟\\mathcal\{D\}that is BAT\-NR wrt ground actionα\\alpha, if𝒟\\mathcal\{D\}is anFO2\\textsc\{FO\}^\{2\}\-BAT wrtα\\alpha, then the progression of𝒟0\\mathcal\{D\}\_\{0\}wrt𝒟,α\\mathcal\{D\},\\alphacan be expressed inFO2\\textsc\{FO\}^\{2\}\.

###### Proof\.

The result is a consequence of Lemma[26](https://arxiv.org/html/2605.12691#Thmtheorem26)\. Since for normal actions, their FO progression is computed by applying Thm\. 5 when forgetting non\-local\-effect fluents, the FO progression is also withinFO2\\textsc\{FO\}^\{2\}if we apply Lemma[26](https://arxiv.org/html/2605.12691#Thmtheorem26)\. Besides, for local\-effect fluents, forgetting them via Eq\. \(4\) leads to a theory that is still inFO2\\textsc\{FO\}^\{2\}by Thm\. 17; this completes the proof\. ∎

### Proof of Theorem[20](https://arxiv.org/html/2605.12691#Thmtheorem20)

###### Theorem\(Restatement of Theorem[20](https://arxiv.org/html/2605.12691#Thmtheorem20)\)\.

Given a BAT𝒟\\mathcal\{D\}that is BAT\-AC wrt ground actionα\\alpha, if𝒟\\mathcal\{D\}is anFO2\\textsc\{FO\}^\{2\}\-BAT wrtα\\alpha, then the progression of𝒟0\\mathcal\{D\}\_\{0\}wrt𝒟,α\\mathcal\{D\},\\alphacan be expressed inFO2\\textsc\{FO\}^\{2\}\.

###### Proof\.

The proof is pretty much like the proof of Thm\. 13 except that we can now use Lemma 19 to show that the formulas generated when forgetting non\-local\-effect fluents can be rewritten to aFO2\\textsc\{FO\}^\{2\}formula that is semi\-definitional wrt another non\-local\-effect fluent\. This process can be iterated over all non\-local\-effect fluents\. For local\-effect fluents, one can use Thm\. 17 to ensure that forgetting them leads to anFO2\\textsc\{FO\}^\{2\}theory as well\. ∎

### Proof of Theorem[23](https://arxiv.org/html/2605.12691#Thmtheorem23)

To prove Theorem[23](https://arxiv.org/html/2605.12691#Thmtheorem23), we need the following lemma\.

###### Lemma 27\.

IfTTis anUTCtheory and semi\-definitional wrtPP, then𝑓𝑜𝑟𝑔𝑒𝑡​\(T,P\)\\mathit\{forget\}\(T,P\)can be expressed inUTC\.

The proof is directly from Thm\. 5\.𝑓𝑜𝑟𝑔𝑒𝑡​\(T,P\)\\mathit\{forget\}\(T,P\)⇔\\LeftrightarrowT′∧⋀ψ∈WSCP,ϕ∈SNCP∀x→\.ψ​\(x→\)⊃ϕ​\(x→\)T^\{\\prime\}\\land\\bigwedge\_\{\\psi\\in\\mathrm\{WSC\}\_\{P\},\\phi\\in\\mathrm\{SNC\}\_\{P\}\}\\forall\\vec\{x\}\.\\psi\(\\vec\{x\}\)\\supset\\phi\(\\vec\{x\}\)\. SinceT′∈UTCT^\{\\prime\}\\in\\textsc\{UTC\}andψ,ϕ\\psi,\\phiare quantifier\-free,𝑓𝑜𝑟𝑔𝑒𝑡​\(T,P\)∈UTC\\mathit\{forget\}\(T,P\)\\in\\textsc\{UTC\}\.

###### Theorem\(Restatement of Theorem[23](https://arxiv.org/html/2605.12691#Thmtheorem23)\)\.

Given a BAT𝒟\\mathcal\{D\}that is BAT\-NR wrt ground actionα\\alpha, if𝒟\\mathcal\{D\}is anUTC\-BAT wrtα\\alpha, then the progression of𝒟0\\mathcal\{D\}\_\{0\}wrt𝒟,α\\mathcal\{D\},\\alphacan be expressed inUTC\.

###### Proof\.

It is a consequence of Lemma[27](https://arxiv.org/html/2605.12691#Thmtheorem27)\. Since for normal actions, their FO progression is computed by applying Thm\. 5 when forgetting non\-local\-effect fluents, the FO progression is also withinUTCif we apply Lemma[27](https://arxiv.org/html/2605.12691#Thmtheorem27)\. Besides, for local\-effect fluents, forgetting them by Eq\. \(4\) leads to a theory that is still inUTCby Thm\. 22; this completes the proof\. ∎

## 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\)\.

## References

- W\. Ackermann \(1935\)Untersuchungen über das Eliminationsproblem der mathematischen Logik\.Mathematische Annalen110\(1\),pp\. 390–413\.Cited by:[§3\.2](https://arxiv.org/html/2605.12691#S3.SS2.p1.18)\.
- M\. Arenas, J\. A\. Baier, J\. S\. Navarro, and S\. Sardiña \(2018\)On the progression of situation calculus universal theories with constants\.InProceedings of the SixteenthInternational Conference on the Principles of Knowledge Representation and Reasoning\(KR 2018\),M\. Thielscher, F\. Toni, and F\. Wolter \(Eds\.\),pp\. 484–493\.Cited by:[§1](https://arxiv.org/html/2605.12691#S1.p3.4),[§5](https://arxiv.org/html/2605.12691#S5.SS0.SSS0.Px3.p3.1),[§6](https://arxiv.org/html/2605.12691#S6.p1.2)\.
- P\. Bernays and M\. Schönfinkel \(1928\)Zum Entscheidungsproblem der mathematischen Logik\.Mathematische Annalen99,pp\. 342–372\.External Links:[Link](https://api.semanticscholar.org/CorpusID:122312654)Cited by:[§5](https://arxiv.org/html/2605.12691#S5.p1.8)\.
- D\. Calvanese, G\. De Giacomo, and M\. Soutchanski \(2015\)On the undecidability of the situation calculus extended with description logic ontologies\.InProceedings of the Twenty\-FourthInternational Joint Conference on Artificial Intelligence\(IJCAI 2015\),Q\. Yang and M\. Wooldridge \(Eds\.\),pp\. 2840–2846\.Cited by:[§6](https://arxiv.org/html/2605.12691#S6.p2.5)\.
- A\. B\. Corrêa and G\. De Giacomo \(2024\)Lifted planning: recent advances in planning using first\-order representations\.InProceedings of the Thirty\-ThirdInternational Joint Conference on Artificial Intelligence\(IJCAI 2024\),K\. Larson \(Ed\.\),pp\. 8010–8019\.Cited by:[§6](https://arxiv.org/html/2605.12691#S6.p3.1)\.
- G\. De Giacomo, Y\. Lespérance, F\. Patrizi, and S\. Vassos \(2016\)Progression and verification of situation calculus agents with bounded beliefs\.Studia Logica104,pp\. 705–739\.Cited by:[§6](https://arxiv.org/html/2605.12691#S6.p1.2)\.
- T\. Eiter and D\. Soldà \(2024\)Computational aspects of progression for temporal equilibrium logic\.InProceedings of the Thirty\-ThirdInternational Joint Conference on Artificial Intelligence\(IJCAI 2024\),K\. Larson \(Ed\.\),pp\. 3342–3350\.Cited by:[§6](https://arxiv.org/html/2605.12691#S6.p1.2)\.
- E\. Grädel, P\. G\. Kolaitis, and M\. Y\. Vardi \(1997\)On the decision problem for two\-variable first\-order logic\.Bulletin of Symbolic Logic3\(1\),pp\. 53–69\.Cited by:[§1](https://arxiv.org/html/2605.12691#S1.p3.4),[§4](https://arxiv.org/html/2605.12691#S4.p1.10),[§4](https://arxiv.org/html/2605.12691#S4.p4.1),[Theorem 15](https://arxiv.org/html/2605.12691#Thmtheorem15)\.
- Y\. Gu and M\. Soutchanski \(2010\)A description logic based situation calculus\.Annals of Mathematics and Artificial Intelligence58\(1–2\),pp\. 3–83\.Cited by:[§6](https://arxiv.org/html/2605.12691#S6.p2.5)\.
- J\. C\. Jung and F\. Wolter \(2021\)Living without beth and craig: definitions and interpolants in the guarded and two\-variable fragments\.InLICS 2021,pp\. 1–14\.Cited by:[§4](https://arxiv.org/html/2605.12691#S4.SS0.SSS0.Px3.p3.6)\.
- G\. Lakemeyer and H\. J\. Levesque \(2002\)Evaluation\-based reasoning with disjunctive information in first\-order knowledge bases\.InProceedings of the EighthInternational Conference on the Principles of Knowledge Representation and Reasoning\(KR 2002\),pp\. 73–81\.Cited by:[§6](https://arxiv.org/html/2605.12691#S6.p1.2)\.
- G\. Lakemeyer and H\. J\. Levesque \(2014\)Decidable reasoning in a fragment of the epistemic situation calculus\.InProceedings of the FourteenthInternational Conference on the Principles of Knowledge Representation and Reasoning\(KR 2014\),T\. Eiter, C\. Baral, and G\. D\. Giacomo \(Eds\.\),pp\. 468–477\.Cited by:[§6](https://arxiv.org/html/2605.12691#S6.p2.5)\.
- H\. J\. Levesque, F\. Pirri, and R\. Reiter \(1998\)Foundations for the situation calculus\.Electron\. Trans\. Artif\. Intell\.2,pp\. 159–178\.External Links:[Link](http://www.ep.liu.se/ej/etai/1998/005/)Cited by:[item 1](https://arxiv.org/html/2605.12691#S2.I1.i1.p1.1)\.
- F\. Lin and R\. Reiter \(1994\)Forget it\!\.InWorking Notes of AAAI Fall Symposium on Relevance,pp\. 154–159\.Cited by:[Theorem 3](https://arxiv.org/html/2605.12691#Thmtheorem3)\.
- F\. Lin and R\. Reiter \(1997\)How to progress a database\.Artificial Intelligence92\(1–2\),pp\. 131–167\.Cited by:[§1](https://arxiv.org/html/2605.12691#S1.p2.1),[§2\.2](https://arxiv.org/html/2605.12691#S2.SS2.p1.1)\.
- D\. Liu and J\. Claßen \(2024\)First\-order progression beyond local\-effect and normal actions\.InProceedings of the Thirty\-ThirdInternational Joint Conference on Artificial Intelligence\(IJCAI 2024\),K\. Larson \(Ed\.\),pp\. 3475–3483\.External Links:[Document](https://dx.doi.org/10.24963/ijcai.2024/385)Cited by:[§1](https://arxiv.org/html/2605.12691#S1.p2.1),[§3\.3](https://arxiv.org/html/2605.12691#S3.SS3.1.p1.6),[§3\.3](https://arxiv.org/html/2605.12691#S3.SS3.p1.8),[§3\.3](https://arxiv.org/html/2605.12691#S3.SS3.p3.19),[§3](https://arxiv.org/html/2605.12691#S3.p1.1),[§6](https://arxiv.org/html/2605.12691#S6.p1.2),[Proof\.](https://arxiv.org/html/2605.12691#Sx1.SSx1.2.p1.5),[Proposition 9](https://arxiv.org/html/2605.12691#Thmtheorem9)\.
- Y\. Liu and G\. Lakemeyer \(2009\)On first\-order definability and computability of progression for local\-effect actions and beyond\.InProceedings of the Twenty\-FirstInternational Joint Conference on Artificial Intelligence\(IJCAI 2009\),C\. Boutilier \(Ed\.\),pp\. 860–866\.Cited by:[§1](https://arxiv.org/html/2605.12691#S1.p2.1),[§3\.1](https://arxiv.org/html/2605.12691#S3.SS1.p1.1),[§3\.1](https://arxiv.org/html/2605.12691#S3.SS1.p2.21),[§3\.1](https://arxiv.org/html/2605.12691#S3.SS1.p2.27),[§3\.1](https://arxiv.org/html/2605.12691#S3.SS1.p2.31),[§3\.2](https://arxiv.org/html/2605.12691#S3.SS2.p3.3),[§6](https://arxiv.org/html/2605.12691#S6.p1.2),[Theorem 5](https://arxiv.org/html/2605.12691#Thmtheorem5)\.
- Y\. Liu and H\. J\. Levesque \(2005\)Tractable reasoning in first\-order knowledge bases with disjunctive information\.InProceedings of the TwentiethNational Conference on Artificial Intelligence\(AAAI 2005\),M\. M\. Veloso and S\. Kambhampati \(Eds\.\),pp\. 639–644\.Cited by:[§6](https://arxiv.org/html/2605.12691#S6.p1.2)\.
- C\. Lutz, U\. Sattler, and F\. Wolter \(2001\)Description logics and the two\-variable fragment\.InWorking Notes of the 2001 International Description Logics Workshop \(DL\-2001\),C\. A\. Goble, D\. L\. McGuinness, R\. Möller, and P\. F\. Patel\-Schneider \(Eds\.\),CEUR Workshop Proceedings, Vol\.49\.Cited by:[§6](https://arxiv.org/html/2605.12691#S6.p2.5)\.
- J\. McCarthy and P\. Hayes \(1969\)Some philosophical problems from the standpoint of artificial intelligence\.InMachine Intelligence 4,B\. Meltzer and D\. Michie \(Eds\.\),pp\. 463–502\.Cited by:[§1](https://arxiv.org/html/2605.12691#S1.p1.7)\.
- R\. Reiter \(2001\)Knowledge in action: logical foundations for specifying and implementing dynamical systems\.MIT Press\.Cited by:[§1](https://arxiv.org/html/2605.12691#S1.p1.7),[§2\.1](https://arxiv.org/html/2605.12691#S2.SS1.p1.19)\.
- S\. Vassos and H\. J\. Levesque \(2013\)How to progress a database III\.Artificial Intelligence195,pp\. 203–221\.External Links:[Document](https://dx.doi.org/10.1016/j.artint.2012.10.005)Cited by:[§2\.2](https://arxiv.org/html/2605.12691#S2.SS2.p1.1),[§2\.2](https://arxiv.org/html/2605.12691#S2.SS2.p3.6)\.
- B\. Zarrieß and J\. Claßen \(2016\)Decidable verification of Golog programs over non\-local effect actions\.InProceedings of the ThirtiethAAAI Conference on Artificial Intelligence\(AAAI 2016\),D\. Schuurmans and M\. Wellman \(Eds\.\),pp\. 1109–1115\.Cited by:[§6](https://arxiv.org/html/2605.12691#S6.p3.1)\.
- B\. Zarrieß \(2018\)Verification of golog programs over description logic actions\.Ph\.D\. Thesis,TU Dresden\.Cited by:[§6](https://arxiv.org/html/2605.12691#S6.p2.5)\.