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

Marianna Girlando (1) , Lutz Strassburger (1)

1 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion

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.

Mots clés: Intuitionistic modal logic; nested sequents; Prolog

Domaines: Logique en informatique [cs.LO]

Marianna Girlando, Lutz Strassburger. MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description). 2020. ⟨hal-02457240v2⟩