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

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

zbMATH Keywords

intuitionistic modal logicnested sequentsprolog

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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

• Prolog
• leanTAP
• NESCOND
• TABLEAUX

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