An Undecidability Proof for the Plan Existence Problem
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Undecidability in Finite Transducers, Defense Systems and Finite Substitutions
In this manuscript we present a detailed proof for undecidability of the equivalence of finite substitutions on regular language $b\{0,1\}^*c$. The proof is based on the works of Leonid P. Lisovik.
Exploring Non-Regular Extensions of Propositional Dynamic Logic with Description-Logics Features
We investigate the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics extending ALC. Our primary objects of interest are ALCreg and ALCvpl, the extens…
From Undecidability of Non-Triviality and Finiteness to Undecidability of Learnability
Machine learning researchers and practitioners steadily enlarge the multitude of successful learning models. They achieve this through in-depth theoretical analyses and experiential heuristics. However, there is no known…
BIG-bench Machine LearningBinary ClassificationDecidability and Undecidability Results for Propositional Schemata
We define a logic of propositional formula schemata adding to the syntax of propositional logic indexed propositions and iterated connectives ranging over intervals parameterized by arithmetic variables. The satisfiabili…
Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. Employing synthetic accounts of enumerability and decidability, we give a full classification of FSAT depending on t…
Relation