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

DOI10.1007/978-3-030-51054-1_25MaRDI QIDQ5049018zbMATH OpenOpenAlexFDO

Authors Marianna Girlando, Lutz Straßburger

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)

Cites work

• Combining monotone and normal modal logic in nested sequents -- with countermodels
• Cut elimination in nested sequents for intuitionistic modal logics
• Cut-elimination and proof search for bi-intuitionistic tense logic
• Cut-free sequent calculi for some tense logics
• Deep sequent systems for modal logic
• Eine Darstellung der Intuitionistischen Logik in der Klassischen
• Focused and Synthetic Nested Sequents
• scientific article; zbMATH DE number 3950488 (Why is no real title available?)
• Label-free modular systems for classical and intuitionistic modal logics
• Label-free proof systems for intuitionistic modal logic IS5
• lean\(T^ AP\): Lean tableau-based deduction
• Maehara-style modal nested calculi
• Modular focused proof systems for intuitionistic modal logics
• Modularisation of sequent calculi for normal and non-normal modalities
• NESCOND: an implementation of nested sequent calculi for conditional logics
• On nested sequents for constructive modal logics
• TABLEAUX: A general theorem prover for modal logics
• The Method of Tree-Hypersequents for Modal Propositional Logic
• Untersuchungen über das logische Schliessen. I

Cited in

(9)

• Local reductions for the modal cube
• Terminating calculi and countermodels for constructive modal logics
• Nested sequents for intuitionistic modal logics via structural refinement
• scientific article; zbMATH DE number 2024634 (Why is no real title available?)
• MOIN
• Mechanising Gödel-Löb provability logic in HOL light
• Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
• Nested sequents or tree-hypersequents -- a survey
• A simple loopcheck for intuitionistic K

Describes a project that uses

Uses Software

• Prolog
• NESCOND
• leanTAP
• TABLEAUX

This page was built for publication: MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5049018)