An Undecidability Proof for the Plan Existence Problem
2026-04-24 • Logic in Computer Science
Logic in Computer ScienceArtificial Intelligence
AI summaryⓘ
The authors studied a problem where you want to find a series of steps (actions) that lead from a starting situation to a goal, described using a type of logic that deals with knowledge and beliefs. They focused on simple conditions for these actions but found that deciding whether such a series of steps exists is impossible to determine with any method. This result means that even with simple action requirements, the problem is very complex and has no general solution. Before this work, it was unknown whether this problem could be solved or not.
plan existence problemmodal logicepistemic statepointed Kripke modelepistemic actionsmodal depthundecidabilitypreconditionspostconditions
Authors
Antonis Achilleos
Abstract
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.