First-Order Progression Stays Polynomial and Decidable for Key Action Classes

Progression — updating a knowledge base to reflect action effects — is a fundamental task in AI reasoning about actions, but it generally requires second-order logic, limiting scalability. In a new paper accepted at IJCAI 2026, Jens Classen and Daxin Liu provide a systematic analysis of the size complexity and decidability of first-order progression. They focus on three increasingly expressive classes of actions — local-effect, normal, and acyclic actions — which were already known to admit first-order progression. The key result: under reasonable assumptions, the size of the progression grows only polynomially for these classes, making them feasible for practical applications.

Beyond size, the authors address decidability. They show that if the initial knowledge base belongs to decidable fragments — specifically two-variable first-order logic (FO²) or universal theories with constants — then the progression remains within the same fragment, ensuring that reasoning queries remain decidable. This bridges theory and practice, as FO² is widely used in description logics and database theory. The paper includes an extended appendix with full proofs, offering a rigorous foundation for future tool development in AI planning and cognitive robotics.