Research
An Undecidability Proof for the Plan Existence Problem
arXiv:2604.22736v1 Announce Type: cross 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
arXiv:2604.22736v1 Announce Type: cross 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.
Related
- Toward a Tractability Frontier for Exact Relevance Certification
- How Hard is it to Decide if a Fact is Relevant to a Query?
- ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning
- Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation
Source: arXiv cs.AI | 2026-04-27