研究动作推理中知识库更新的规模与可判定性，发现其增长可控且可计算。
On the Size Complexity and Decidability of First-Order Progression
- 基于情景演算框架，分析三类动作的前向推理规模
- 在合理假设下，前向推理结果仅多项式增长
- 适用于可判定逻辑片段，适合形式化验证应用
动作效应更新（Progression）通常需要二阶逻辑。长期以来，通过限制知识库或动作效应，寻找一阶可处理的特殊情况是动作推理的核心问题。已知局部效应、正则和无环三类动作均支持一阶进展。然而，此类进展的规模分析长期缺失。本文在情景演算框架下证明，在合理假设下，这三类动作的一阶进展规模仅呈多项式增长。此外，当知识库属于可判定片段（如二元一阶逻辑或带常量的全称理论）时，进展仍保持在同一线段内，确保了可判定性与实际应用可行性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。