Girlando, M., Kuznets, R., Marin, S., Morales, M., & Straßburger, L. (2023, September 27). Intuitionistic S4 and its decidability [Conference Presentation]. Mosaic Workshop 2023, Wien, Austria. http://hdl.handle.net/20.500.12708/192652
E191-02 - Forschungsbereich Embedded Computing Systems
-
Date (published):
27-Sep-2023
-
Event name:
Mosaic Workshop 2023
-
Event date:
26-Sep-2023 - 29-Sep-2023
-
Event place:
Wien, Austria
-
Keywords:
decidability; Intuitionistic modal logic; labeled proof systems
en
Abstract:
We present a decision procedure for IS4, an intuitionistic modal logic first formulated by Fisher Servi. The logic has two independent modalities and is interpreted over birelational Kripke models. Unlike other intuitionistic modal logics, the problem of decidability of IS4 has been open for almost thirty years, since it has been posed in Simpson’s PhD thesis in 1994. Our result is obtained by defining a proof-search algorithm based on a labelled sequent calculus that explicitly incorporates the two accessibility relations of Kripke models for the logic. The search algorithm outputs either a proof or a finite countermodel, thus additionally establishing the finite model property for IS4.
en
Project title:
Reasoning about Knowledge in Byzantine Distributed Systems: P 33600-N (FWF - Österr. Wissenschaftsfonds)
-
Research Areas:
Computer Engineering and Software-Intensive Systems: 100%
