Dynamic Term-Modal Logics for Epistemic Planning

Classical planning frameworks are built on first-order languages. The first-order expressive power is desirable for compactly representing actions via schemas, and for specifying goal formulas such as $\neg\exists x\mathsf{blocks\_door}(x)$. In contrast, several recent epistemic planning frameworks build on propositional modal logic. The modal expressive power is desirable for investigating planning problems with epistemic goals such as $K_{a}\neg\mathsf{problem}$. The present paper presents an epistemic planning framework with first-order expressiveness of classical planning, but extending fully to the epistemic operators. In this framework, e.g. $\exists xK_{x}\exists y\mathsf{blocks\_door}(y)$ is a formula. Logics with this expressive power are called "term-modal" in the literature. This paper presents a rich but well-behaved semantics for term-modal logic. The semantics are given a dynamic extension using first-order "action models" allowing for epistemic planning, and it is shown how corresponding "action schemas" allow for a very compact action representation. Concerning metatheory, the paper defines axiomatic normal term-modal logics, shows a Canonical Model Theorem-like result, present non-standard frame characterization formulas, shows decidability for the finite agent case, and shows a general completeness result for the dynamic extension by reduction axioms.