Dynamic Term-Modal Logics for First-Order Epistemic Planning

Many 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 quantified conditions such as negexists xmathsfblocksdoor(x). In contrast, several recent epistemic planning frameworks are built on propositional epistemic logic. The epistemic language is useful to describe planning problems involving higher-order reasoning or epistemic goals such as Kanegmathsfproblem. This paper develops a first-order version of Dynamic Epistemic Logic (DEL). In this framework, for example, exists xKxexists ymathsfblocksdoor(y) is a formula. The formalism combines the strengths of DEL (higher-order reasoning) with those of first-order logic (lifted representation) to model multi-agent epistemic planning. The paper introduces an epistemic language with a possible-worlds semantics, followed by novel dynamics given by first-order action models and their execution via product updates. Taking advantage of the first-order machinery, epistemic action schemas are defined to provide compact, problem-independent domain descriptions, in the spirit of PDDL. Concerning metatheory, the paper defines axiomatic normal term-modal logics, shows a Canonical Model Theorem-like result which allows establishing completeness through frame characterization formulas, shows decidability for the finite agent case, and shows a general completeness result for the dynamic extension by reduction axioms.