Skip to Main content Skip to Navigation
Book sections

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 :
Book sections
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-02457240
Contributor : Lutz Straßburger <>
Submitted on : Friday, October 30, 2020 - 10:32:27 AM
Last modification on : Saturday, October 31, 2020 - 3:30:59 AM

File

modal_prover.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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

Share

Metrics

Record views

31

Files downloads

81