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

[img] 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)

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.

Item Type:

Book Section (Book Chapter)

Division/Institute:

08 Faculty of Science > Institute of Computer Science (INF) > Logic and Theory Group (LTG)
08 Faculty of Science > Institute of Computer Science (INF)

UniBE Contributor:

Zenger, Lukas Matthias

Subjects:

000 Computer science, knowledge & systems
500 Science > 510 Mathematics

ISBN:

978-1-84890-413-2

Series:

Advances in Modal Logic

Publisher:

College Publications

Language:

English

Submitter:

Atefeh Rohani

Date Deposited:

25 Jan 2023 10:53

Last Modified:

25 Jan 2023 23:28

Uncontrolled Keywords:

Common knowledge, S5 multi-modal logic, analytic proof systems, cyclic proofs, proof search games.

BORIS DOI:

10.48350/177367

URI:

https://boris.unibe.ch/id/eprint/177367

Actions (login required)

Edit item Edit item
Provide Feedback