pith. sign in

arxiv: 2605.12691 · v1 · pith:Z7G6OGXMnew · submitted 2026-05-12 · 💻 cs.AI

On the Size Complexity and Decidability of First-Order Progression

Jens Classen , Daxin Liu This is my paper

Pith reviewed 2026-05-14 20:13 UTC · model grok-4.3

classification 💻 cs.AI
keywords first-order progressionsituation calculusaction effectspolynomial sizedecidabilityknowledge base updatelocal-effect actions
0
0 comments X

The pith

First-order progression for local-effect, normal, and acyclic actions grows only polynomially under reasonable assumptions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that updating a knowledge base after actions can stay within first-order logic for three restricted action classes: local-effect, normal, and acyclic. For these classes the progressed knowledge base is a first-order formula whose size grows only polynomially with the original knowledge base. The result holds under reasonable assumptions on the knowledge base and effects. When the starting knowledge base lies in a decidable fragment such as two-variable first-order logic or universal theories with constants, the progressed version stays inside the same fragment and therefore remains decidable.

Core claim

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.

What carries the argument

local-effect, normal, and acyclic actions, which admit first-order progression formulas whose size is polynomial in the knowledge base.

If this is right

  • Progression becomes feasible for large knowledge bases without switching to second-order logic.
  • Decidability carries over automatically when the initial knowledge base is in two-variable first-order logic or universal theories with constants.
  • Practical implementations of action reasoning can rely on these size bounds for the listed action classes.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same polynomial bound may hold for analogous restricted actions in other action formalisms if the local-effect or acyclicity conditions can be stated similarly.
  • Automated theorem provers for the preserved fragments could be applied directly to the progressed formulas without additional preprocessing.
  • Complexity results for still more expressive action classes might be obtained by relaxing the restrictions one at a time while tracking size growth.

Load-bearing premise

The actions must belong to the local-effect, normal, or acyclic classes and the knowledge base must meet the unspecified reasonable assumptions that produce the polynomial size bound.

What would settle it

An explicit knowledge base together with one action from any of the three classes for which every first-order progression formula has size superpolynomial in the size of the original knowledge base.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The manuscript analyzes first-order progression in the Situation Calculus for local-effect, normal, and acyclic actions. It establishes polynomial size growth of the progressed knowledge base under specified assumptions on the knowledge base and action effects. It further proves that progression preserves membership in decidable fragments such as two-variable first-order logic and universal theories with constants.

Significance. This work is significant for bridging theoretical results on first-order progression with practical considerations of computational complexity and decidability. The explicit inductive constructions on syntactic complexity of effects provide a clear mechanism for the polynomial bound, and the variable-counting arguments ensure fragment preservation without increasing quantifier rank or introducing new variables. These contributions enable more efficient implementations in reasoning systems for dynamic domains.

minor comments (3)
  1. [Abstract] Abstract: the phrase 'reasonable assumptions' should include a direct pointer to the precise restrictions (local-effect, normal, acyclic) defined in §3, as this is load-bearing for the polynomial claim.
  2. [§4.2] §4.2, inductive construction for acyclic actions: the degree of the polynomial depends on the depth of the dependency graph; an explicit statement of this dependence would strengthen the size bound.
  3. [§5.1] §5.1, variable-counting argument for FO²: while the argument is correct, an example showing how a progressed formula stays within two variables would aid readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, recognition of the significance of our results on polynomial-size first-order progression for local-effect, normal, and acyclic actions, and the recommendation for minor revision. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper derives polynomial size bounds for first-order progression via explicit inductive constructions on the syntactic complexity of effects for the defined action classes (local-effect, normal, acyclic). Fragment preservation arguments rely on variable-counting that does not increase quantifier rank or introduce new variables, remaining within standard situation calculus semantics. No load-bearing steps reduce to self-definitions, fitted inputs renamed as predictions, or self-citation chains; the central claims are established by direct syntactic analysis independent of the target results.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard Situation Calculus axioms for actions and situations plus the syntactic restrictions defining local-effect, normal, and acyclic actions; no free parameters or invented entities are introduced.

axioms (2)
  • domain assumption Standard axioms of the Situation Calculus for representing fluents, actions, and situations
    The framework used throughout the paper for defining progression.
  • domain assumption Syntactic definitions of local-effect, normal, and acyclic actions
    These restrictions enable first-order progression and are load-bearing for the polynomial bound.

pith-pipeline@v0.9.0 · 5432 in / 1304 out tokens · 100062 ms · 2026-05-14T20:13:17.308661+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages

  1. [1]

    Untersuchungen ¨uber das Eliminationsproblem der mathematischen Logik

    [Ackermann, 1935] Wilhelm Ackermann. Untersuchungen ¨uber das Eliminationsproblem der mathematischen Logik. Mathematische Annalen, 110(1):390–413,

    work page 1935

  2. [2]

    Baier, Juan S

    [Arenaset al., 2018 ] Marcelo Arenas, Jorge A. Baier, Juan S. Navarro, and Sebastian Sardi ˜na. On the progres- sion of situation calculus universal theories with constants. In Michael Thielscher, Francesca Toni, and Frank Wolter, editors,Proceedings of the Sixteenth International Confer- ence on the Principles of Knowledge Representation and Reasoning (K...

    work page 2018

  3. [3]

    Zum Entscheidungsproblem der mathematis- chen Logik.Mathematische Annalen, 99:342–372,

    [Bernays and Sch¨onfinkel, 1928] Paul Bernays and Moses Sch¨onfinkel. Zum Entscheidungsproblem der mathematis- chen Logik.Mathematische Annalen, 99:342–372,

    work page 1928

  4. [4]

    On the undecidability of the situation calculus extended with description logic ontologies

    [Calvaneseet al., 2015 ] Diego Calvanese, Giuseppe De Gi- acomo, and Mikhail Soutchanski. On the undecidability of the situation calculus extended with description logic ontologies. In Qiang Yang and Michael Wooldridge, edi- tors,Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015), pages 2840–2846. AAAI Press,

    work page 2015

  5. [5]

    Corr ˆea and Giuseppe De Giacomo

    [Corrˆea and De Giacomo, 2024] Augusto B. Corr ˆea and Giuseppe De Giacomo. Lifted planning: Recent advances in planning using first-order representations. In Kate Lar- son, editor,Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI 2024), pages 8010–8019. ijcai.org,

    work page 2024

  6. [6]

    Progres- sion and verification of situation calculus agents with bounded beliefs.Studia Logica, 104:705–739,

    [De Giacomoet al., 2016 ] Giuseppe De Giacomo, Yves Lesp´erance, Fabio Patrizi, and Stavros Vassos. Progres- sion and verification of situation calculus agents with bounded beliefs.Studia Logica, 104:705–739,

    work page 2016

  7. [7]

    Computational aspects of progression for temporal equi- librium logic

    [Eiter and Sold`a, 2024] Thomas Eiter and Davide Sold `a. Computational aspects of progression for temporal equi- librium logic. In Kate Larson, editor,Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI 2024), pages 3342–3350. ijcai.org,

    work page 2024

  8. [8]

    Kolaitis, and Moshe Y

    [Gr¨adelet al., 1997 ] Erich Gr¨adel, Phokion G. Kolaitis, and Moshe Y . Vardi. On the decision problem for two-variable first-order logic.Bulletin of Symbolic Logic, 3(1):53–69,

    work page 1997

  9. [9]

    A description logic based situation calcu- lus.Annals of Mathematics and Artificial Intelligence, 58(1–2):3–83,

    [Gu and Soutchanski, 2010] Yilan Gu and Mikhail Soutchanski. A description logic based situation calcu- lus.Annals of Mathematics and Artificial Intelligence, 58(1–2):3–83,

    work page 2010

  10. [10]

    Living without beth and craig: Definitions and interpolants in the guarded and two-variable fragments

    [Jung and Wolter, 2021] Jean Christoph Jung and Frank Wolter. Living without beth and craig: Definitions and interpolants in the guarded and two-variable fragments. In LICS 2021, pages 1–14. IEEE,

    work page 2021

  11. [11]

    Levesque

    [Lakemeyer and Levesque, 2002] Gerhard Lakemeyer and Hector J. Levesque. Evaluation-based reasoning with dis- junctive information in first-order knowledge bases. In Proceedings of the Eighth International Conference on the Principles of Knowledge Representation and Reasoning (KR 2002), pages 73–81. AAAI Press,

    work page 2002

  12. [12]

    Levesque

    [Lakemeyer and Levesque, 2014] Gerhard Lakemeyer and Hector J. Levesque. Decidable reasoning in a fragment of the epistemic situation calculus. In Thomas Eiter, Chitta Baral, and Giuseppe De Giacomo, editors,Proceedings of the Fourteenth International Conference on the Principles of Knowledge Representation and Reasoning (KR 2014), pages 468–477. AAAI Press,

    work page 2014

  13. [13]

    Levesque, Fiora Pirri, and Raymond Reiter

    [Levesqueet al., 1998 ] Hector J. Levesque, Fiora Pirri, and Raymond Reiter. Foundations for the situation calculus. Electron. Trans. Artif. Intell., 2:159–178,

    work page 1998

  14. [14]

    Forget it! InWorking Notes of AAAI Fall Symposium on Rele- vance, pages 154–159,

    [Lin and Reiter, 1994] Fangzhen Lin and Ray Reiter. Forget it! InWorking Notes of AAAI Fall Symposium on Rele- vance, pages 154–159,

    work page 1994

  15. [15]

    How to progress a database.Artificial Intelligence, 92(1– 2):131–167,

    [Lin and Reiter, 1997] Fangzhen Lin and Raymond Reiter. How to progress a database.Artificial Intelligence, 92(1– 2):131–167,

    work page 1997

  16. [16]

    First- order progression beyond local-effect and normal actions

    [Liu and Claßen, 2024] Daxin Liu and Jens Claßen. First- order progression beyond local-effect and normal actions. In Kate Larson, editor,Proceedings of the Thirty-Third In- ternational Joint Conference on Artificial Intelligence (IJ- CAI 2024), pages 3475–3483. ijcai.org,

    work page 2024

  17. [17]

    On first-order definability and computability of progression for local-effect actions and beyond

    [Liu and Lakemeyer, 2009] Yongmei Liu and Gerhard Lake- meyer. On first-order definability and computability of progression for local-effect actions and beyond. In Craig Boutilier, editor,Proceedings of the Twenty-First Interna- tional Joint Conference on Artificial Intelligence (IJCAI 2009), pages 860–866. AAAI Press,

    work page 2009

  18. [18]

    Levesque

    [Liu and Levesque, 2005] Yongmei Liu and Hector J. Levesque. Tractable reasoning in first-order knowledge bases with disjunctive information. In Manuela M. Veloso and Subbarao Kambhampati, editors,Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI 2005), pages 639–644. AAAI Press,

    work page 2005

  19. [19]

    Description logics and the two-variable frag- ment

    [Lutzet al., 2001 ] Carsten Lutz, Ulrike Sattler, and Frank Wolter. Description logics and the two-variable frag- ment. In Carole A. Goble, Deborah L. McGuinness, Ralf M¨oller, and Peter F. Patel-Schneider, editors,Working Notes of the 2001 International Description Logics Work- shop (DL-2001), volume 49 ofCEUR Workshop Proceed- ings. CEUR-WS.org,

    work page 2001

  20. [20]

    Some philosophical problems from the standpoint of artificial intelligence

    [McCarthy and Hayes, 1969] John McCarthy and Patrick Hayes. Some philosophical problems from the standpoint of artificial intelligence. In B. Meltzer and D. Michie, ed- itors,Machine Intelligence 4, pages 463–502. American Elsevier, New York,

    work page 1969

  21. [21]

    MIT Press,

    [Reiter, 2001] Raymond Reiter.Knowledge in Action: Logi- cal Foundations for Specifying and Implementing Dynam- ical Systems. MIT Press,

    work page 2001

  22. [22]

    Levesque

    [Vassos and Levesque, 2013] Stavros Vassos and Hector J. Levesque. How to progress a database III.Artificial In- telligence, 195:203–221,

    work page 2013

  23. [23]

    Decidable verification of Golog programs over non-local effect actions

    [Zarrieß and Claßen, 2016] Benjamin Zarrieß and Jens Claßen. Decidable verification of Golog programs over non-local effect actions. In Dale Schuurmans and Michael Wellman, editors,Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (AAAI 2016), pages 1109–1115. AAAI Press,

    work page 2016

  24. [24]

    PhD thesis, TU Dresden, 2018

    [Zarrieß, 2018] Benjamin Zarrieß.Verification of Golog Pro- grams over Description Logic Actions. PhD thesis, TU Dresden, 2018

    work page 2018