一阶进展的规模复杂性与可判定性
本文研究了推理动作中知识库更新的关键任务——进展（progression）。进展通常需要二阶逻辑，但通过限制知识库或动作效果，可识别出一阶逻辑的特殊情况。作者利用情境演算框架，证明了在合理假设下，局部效应、正规和循环动作这三类表达力递增的动作类，其一阶进展仅呈多项式增长。此外，当知识库属于可判定片段（如二变量一阶逻辑或带常数的全称理论）时，进展仍保持在同一片段内，保证了可判定性和实际应用性。
在人工智能领域，推理动作（reasoning about actions）是一个核心议题，其中进展（progression）任务旨在根据动作效果更新知识库。长期以来，进展通常需要二阶逻辑，这在实际应用中带来了计算挑战。然而，通过限制知识库或动作效果，研究人员发现存在一阶逻辑的特殊情况，使得进展可以用一阶逻辑表达。此前已知局部效应（local-effect）、正规（normal）和循环（acyclic）这三类动作支持一阶进展，但这些进展的规模复杂性一直缺乏系统分析。
在IJCAI 2026上发表的论文《On the Size Complexity and Decidability of First-Order Progression》中，作者Jens Classen和Daxin Liu利用情境演算（Situation Calculus）框架，对这一问题进行了深入研究。他们证明，在合理假设下，上述三类动作的一阶进展仅呈多项式增长，而非指数级爆炸。这一发现对于实际应用至关重要，因为多项式增长意味着算法可扩展。
此外，论文还探讨了可判定性问题。当知识库属于某些可判定逻辑片段时，例如二变量一阶逻辑（two-variable first-order logic）或带常数的全称理论（universal theories with constants），进展后的知识库仍属于同一片段，从而保证了可判定性。这意味着在这些情况下，进展后的推理仍然是可行的。
该研究填补了进展理论中的空白，为设计和实现高效的进展算法提供了理论基础。论文还附有包含更多证明的附录，为后续研究提供了参考。这项工作不仅推动了推理动作的理论发展，也为人工智能中的自动化规划、机器人控制等应用领域带来了潜在影响。