Nested sequents for intuitionistic modal logics via structural refinement

DOI10.1007/978-3-030-86059-2_24OpenAlexW3204445992MaRDI QIDQ2142093

Tim S. Lyon

Publication date: 25 May 2022

Full work available at URL: https://arxiv.org/abs/2107.01998

zbMATH Keywords

proof theoryrefinementintuitionistic modal logicnested sequentpropagation rulelabelled sequentbi-relational model

Mathematics Subject Classification ID

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

Related Items (1)

Nested sequents for intermediate logics: the case of Gödel-Dummett logics

Uses Software

• MiniML
• MOIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modal interpolation via nested sequents
• Deep sequent systems for modal logic
• Proof methods for modal and intuitionistic logics
• Cut-free sequent calculi for some tense logics
• On an intuitionistic modal logic
• From display to labelled proofs for tense logics
• A semantical view of proof systems
• Tableau methods of proof for modal logics
• Label-free natural deduction systems for intuitionistic and classical modal logics
• On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics
• A modal analysis of staged computation
• CUT ELIMINATION FOR PROPOSITIONAL DYNAMIC LOGIC WITHOUT
• Tree-sequent calculi and decision procedures for intuitionistic modal logics
• Cut Elimination in Nested Sequents for Intuitionistic Modal Logics
• Recursive Unsolvability of a problem of Thue
• On the correspondence between nested calculi and semantic systems for intuitionistic logics
• Display to Labeled Proofs and Back Again for Tense Logics
• MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)

This page was built for publication: Nested sequents for intuitionistic modal logics via structural refinement