The undecidability of arbitrary arrow update logic

DOI10.1016/J.TCS.2017.07.018MaRDI QIDQ2404071zbMATH OpenOpenAlexFDO

Authors Wiebe van der Hoek, Louwe B. Kuijer, Hans van Ditmarsch

Publication date 12 September 2017

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1609.05686

zbMATH Keywords

dynamic epistemic logicsatisfiabilityundecidabilityupdate logics

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Logics of knowledge and belief (including belief change) (03B42) Modal logic (including the logic of norms) (03B45)

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.

Recommendations

• Arbitrary arrow update logic with common knowledge is neither RE nor co-RE
• Undecidability for arbitrary public announcement logic
• A Universally Defined Undecidable Unimodal Logic
• Arbitrary arrow update logic
• scientific article; zbMATH DE number 1047504

Cites work

• `Knowable' as `known after an announcement'
• Arbitrary action model logic and action model synthesis
• Arbitrary arrow update logic
• Arrow update logic
• Dynamic epistemic logic
• Group announcement logic
• Logics of public communications
• Refinement modal logic
• The logic of public announcements, common knowledge, and private suspicions
• The undecidability of quantified announcements
• The undecidability of the domino problem
• Undecidability for arbitrary public announcement logic

Cited in

(9)

• Positive announcements
• Arrow update synthesis
• Decidable subsets of open logic and an algorithm for R-calculus
• Arbitrary arrow update logic with common knowledge is neither RE nor co-RE
• Arbitrary arrow update logic
• Quantifying over Boolean announcements
• Partitioning Kripke frames of finite height
• To be announced
• About the complete axiomatization of dynamic extensions of arrow logic

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)