The undecidability of arbitrary arrow update logic

From MaRDI portal



Abstract: Arbitrary Arrow Update Logic is a dynamic modal logic that uses an arbitrary arrow update modality to quantify over all arrow updates. Some properties of this logic have already been established, but until now it remained an open question whether the logic's satisfiability problem is decidable. Here, we show that the satisfiability problem of Arbitrary Arrow Update Logic is co-RE hard, and therefore undecidable, by a reduction of the tiling problem.


Arbitrary arrow update logic (AAUL) [\textit{H. van Ditmarsch} et al., Artif. Intell. 242, 80--106 (2017; Zbl 1392.68396)] can be considered a dynamic modal logic with a modality to quantify over arrow updates. The authors introduce and develop the syntax and semantics of AAUL, provide a brief definition of the tiling problem and show that it can be encoded in the corresponding satisfiability problem.











This page was built for publication: The undecidability of arbitrary arrow update logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2404071)