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.
翻译:计划存在问题询问:给定一个以模态逻辑公式形式表示的目标、一个初始认知状态(一个带指点的克里普克模型)以及一组认知动作,是否存在一个可应用的行动序列以达到该目标。我们证明,即使认知动作的前提条件的模态深度至多为1,且没有后置条件,计划存在问题仍然是不可判定的。此前,该问题的(不)可判定性是未知的。