On the Size Complexity and Decidability of First-Order Progression

关于一阶演进的规模复杂性与可判定性

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. 摘要： 演进（Progression）是指更新知识库以反映动作影响的任务，通常需要二阶逻辑。通过限制知识库或动作影响来识别一阶特殊情况，长期以来一直是动作推理领域的核心课题。

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. 已知局部影响（local-effect）、正规（normal）和无环（acyclic）动作这三类表达能力递增的动作，均允许一阶演进。然而，对于实际应用至关重要的此类演进规模的系统性分析，此前一直处于缺失状态。

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. 在本文中，我们利用情境演算（Situation Calculus）框架证明，在合理的假设下，这些动作类的一阶演进仅呈多项式增长。

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. 此外，我们还证明了当知识库（KB）属于可判定片段（如双变量一阶逻辑或带有常量的全称理论）时，演进结果仍保持在同一片段内，从而确保了其可判定性和实际应用价值。