Skip to Main content Skip to Navigation
Conference papers

MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)

Marianna Girlando 1 Lutz Straßburger 1
1 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : We present a simple Prolog prover for intuitionistic modal logics based on nested sequent proof systems. We have implemented single-conclusion systems (Gentzen-style) and multi-conclusion systems (Maehara-style) for all logics in the intuitionistic modal IS5-cube. While the single-conclusion system are better investigated and have an internal cut-elimination, the multi-conclusion systems can provide a counter model in case the proof search fails. To our knowledge this is the first automated theorem prover for intuitionistic modal logics. For wider us-ability of our system, we also implemented all classical normal modal logics in the S5-cube.
Document type :
Conference papers
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Friday, October 30, 2020 - 10:32:27 AM
Last modification on : Saturday, May 1, 2021 - 3:41:42 AM


Files produced by the author(s)



Marianna Girlando, Lutz Straßburger. MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description). IJCAR 2020 - 10th International Joint Conference, Jul 2020, Paris, France. pp.398-407, ⟨10.1007/978-3-030-51054-1_25⟩. ⟨hal-02457240v3⟩



Record views


Files downloads