Dynamic term-modal logics for first-order epistemic planning
Research output: Contribution to journal › Journal article › Research › peer-review
Standard
Dynamic term-modal logics for first-order epistemic planning. / Occhipinti Liberman, Andrés; Achen, Andreas; Rendsvig, Rasmus Kræmmer.
In: Artificial Intelligence, Vol. 286, 103305, 09.2020.Research output: Contribution to journal › Journal article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - Dynamic term-modal logics for first-order epistemic planning
AU - Occhipinti Liberman, Andrés
AU - Achen, Andreas
AU - Rendsvig, Rasmus Kræmmer
N1 - Correction: https://doi.org/10.1016/j.artint.2023.103969
PY - 2020/9
Y1 - 2020/9
N2 - 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 ¬∃xblocks_door(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 Ka¬problem. This paper develops a first-order version of Dynamic Epistemic Logic (DEL). In this framework, for example, ∃xKx∃yblocks_door(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.
AB - 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 ¬∃xblocks_door(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 Ka¬problem. This paper develops a first-order version of Dynamic Epistemic Logic (DEL). In this framework, for example, ∃xKx∃yblocks_door(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.
KW - Dynamic epistemic logic
KW - Epistemic planning
KW - Multi-agent systems
KW - Planning formalisms
KW - Term-modal logic
U2 - 10.1016/j.artint.2020.103305
DO - 10.1016/j.artint.2020.103305
M3 - Journal article
AN - SCOPUS:85086372482
VL - 286
JO - Artificial Intelligence
JF - Artificial Intelligence
SN - 0004-3702
M1 - 103305
ER -
ID: 255736665