Satisfiability of Arbitrary Public Announcement Logic with Common Knowledge is Σ^1_1-hard

Galimullin, Rustam and Kuijer, Louwe B ORCID: 0000-0001-6696-9023 (2023) Satisfiability of Arbitrary Public Announcement Logic with Common Knowledge is Σ^1_1-hard. In: TARK-2023.

PDF
APALC_and_friends.pdf - Author Accepted Manuscript
Download (277kB) | Preview

Official URL: http://dx.doi.org/10.4204/eptcs.379.21

Abstract

Arbitrary Public Announcement Logic with Common Knowledge (APALC) is an extension of Public Announcement Logic with common knowledge modality and quantifiers over announcements. We show that the satisfiability problem of APALC on S5-models, as well as that of two other related logics with quantification and common knowledge, is Σ11-hard. This implies that neither the validities nor the satisfiable formulas of APALC are recursively enumerable. Which, in turn, implies that APALC is not finitely axiomatisable.

Item Type:	Conference or Workshop Item (Unspecified)
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	15 May 2023 08:51
Last Modified:	04 Mar 2024 09:17
DOI:	10.4204/eptcs.379.21
Related URLs:	Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3170260