证明了在特定条件下规划存在性问题不可判定，揭示了认知推理的深层计算极限。
An Undecidability Proof for the Plan Existence Problem
- 基于模态深度为1的行动前提，构造不可判定性归约
- 即使无后置条件，规划存在性仍无法判断
- 对认知系统形式化验证具有根本性意义
规划存在性问题要求：给定一个模态逻辑形式的目标、初始认知状态（带标记的克里普克模型）以及一组认知动作，判断是否存在一系列可执行的动作序列以达成目标。本文证明，即使动作的先决条件模态深度不超过1且无后置条件，该问题依然不可判定。此前该问题的可判定性尚不明确。
原文摘要 · Abstract (English)
The plan existence problem asks, given a goal in the form of a formula in modal logic, an initial epistemic state (a pointed Kripke model), and a set of epistemic actions, whether there exists a sequence of actions that can be applied to reach the goal. We prove that even in the case where the preconditions of the epistemic actions have modal depth at most 1, and there are no postconditions, the plan existence problem is undecidable. The (un)decidability of this problem was previously unknown.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。