An analytic proof system for common knowledge logic over S5

Rooduijn, Jan; Zenger, Lukas (2022). An analytic proof system for common knowledge logic over S5. In: Fernández-Duque, David; Palmigiano, Alessandra; Pinchinat, Sophie (eds.) Proceedings of AiML 2022. Advances in Modal Logic: Vol. 14 (pp. 659-680). College Publications

Text An_analytic_proof_system_for_CKL_over_S5.pdf - Published Version Restricted to registered users only Available under License Publisher holds Copyright. Download (457kB) | Request a copy

In this paper we present an analytic proof system for multi-modal logic with common-knowledge over S5 (called S5-CKL). The system is an annotated cyclic calculus manipulating two-sided Gentzen sequents and extending a known system for multi-modalS5. First a direct argument is used to show that the system is sound. Using a canonical model construction, we then show that the system is analytically complete. In particular, the use of the cut-rule is restricted to analytic cuts. Exploiting this analyticity, we then reduce the provability problem of a given sequent to the problem of solving a certain parity game. As a consequence we obtain an optimal decision procedure for proof search and thereby for the validity problem of S5-CKL.

Interest & Impact

Downloads

3 since deposited on 25 Jan 2023
3 in the past 12 months

Citations

5 Citations in Web of Science ®
6 Citations in Scopus

Search

in Google Scholar™

Services

Actions (login required)

Edit item

Actions (login required)

Edit item