Print Email Facebook Twitter Completeness for game logic Title Completeness for game logic Author Enqvist, Sebastian (Stockholm University) Hansen, H.H. (TU Delft Energie and Industrie) Kupke, Clemens (University of Strathclyde) Marti, Johannes (University of Bremen) Venema, Yde (Universiteit van Amsterdam) Date 2019 Abstract Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of propositional dynamic logic (PDL) for reasoning about outcomes that players can force in determined 2-player games. Semantically, the generalisation from programs to games is mirrored by moving from Kripke models to monotone neighbourhood models. Parikh proposed a natural PDL-style Hilbert system which was easily proved to be sound, but its completeness has thus far remained an open problem. In this paper, we introduce a cut-free sequent calculus for game logic, and two cut-free sequent calculi that manipulate annotated formulas, one for game logic and one for the monotone μ-calculus, the variant of the polymodal μ-calculus where the semantics is given by monotone neighbourhood models instead of Kripke structures. We show these systems are sound and complete, and that completeness of Parikh's axiomatization follows. Our approach builds on recent ideas and results by Afshari Leigh (LICS 2017) in that we obtain completeness via a sequence of proof transformations between the systems. A crucial ingredient is a validity-preserving translation from game logic to the monotone μ-calculus. To reference this document use: http://resolver.tudelft.nl/uuid:e3f48630-7faa-4569-8f5f-543f098d1df0 DOI https://doi.org/10.1109/LICS.2019.8785676 Publisher Institute of Electrical and Electronics Engineers (IEEE) ISBN 9781728136080 Source 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, 2019-June Event 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, 2019-06-24 → 2019-06-27, Vancouver, Canada Part of collection Institutional Repository Document type conference paper Rights © 2019 Sebastian Enqvist, H.H. Hansen, Clemens Kupke, Johannes Marti, Yde Venema Files PDF Completeness_for_Game_Logic.pdf 526.63 KB Close viewer /islandora/object/uuid:e3f48630-7faa-4569-8f5f-543f098d1df0/datastream/OBJ/view