一階進展的規模複雜性與可判定性
本文研究了推理動作中知識庫更新的關鍵任務——進展（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），進展後的知識庫仍屬於同一片段，從而保證了可判定性。這意味著在這些情況下，進展後的推理仍然是可行的。
該研究填補了進展理論中的空白，為設計和實現高效的進展演算法提供了理論基礎。論文還附有包含更多證明的附錄，為後續研究提供了參考。這項工作不僅推動了推理動作的理論發展，也為人工智慧中的自動化規劃、機器人控制等應用領域帶來了潛在影響。