MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
From MaRDI portal
Publication:5049018
DOI10.1007/978-3-030-51054-1_25OpenAlexW3017391521MaRDI QIDQ5049018
Lutz Straßburger, Marianna Girlando
Publication date: 9 November 2022
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-030-51054-1_25
Related Items
Terminating calculi and countermodels for constructive modal logics ⋮ Nested sequents for intuitionistic modal logics via structural refinement ⋮ Mechanising Gödel-Löb provability logic in HOL light ⋮ MOIN ⋮ Local reductions for the modal cube
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Deep sequent systems for modal logic
- TABLEAUX: A general theorem prover for modal logics
- Cut-free sequent calculi for some tense logics
- Maehara-style modal nested calculi
- Untersuchungen über das logische Schliessen. I
- lean\(T^ AP\): Lean tableau-based deduction
- Combining monotone and normal modal logic in nested sequents -- with countermodels
- Focused and Synthetic Nested Sequents
- Label-Free Proof Systems for Intuitionistic Modal Logic IS5
- NESCOND: An Implementation of Nested Sequent Calculi for Conditional Logics
- On Nested Sequents for Constructive Modal Logics
- The Method of Tree-Hypersequents for Modal Propositional Logic
- Modularisation of Sequent Calculi for Normal and Non-normal Modalities
- Cut Elimination in Nested Sequents for Intuitionistic Modal Logics
- Modular Focused Proof Systems for Intuitionistic Modal Logics
- Eine Darstellung der Intuitionistischen Logik in der Klassischen