Modular focused proof systems for intuitionistic modal logics

DOI10.4230/LIPICS.FSCD.2016.16MaRDI QIDQ5369481zbMATH OpenOpenAlexFDO

Authors Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger

Publication date 17 October 2017

Full work available at URL https://hal.inria.fr/hal-01417603

zbMATH Keywords

cut eliminationfocusingintuitionistic modal logicnested sequentsproof search

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Focused and Synthetic Nested Sequents
• Proof search in nested sequent calculi
• Focusing and Polarization in Intuitionistic Logic
• Structural focalization
• A semantical analysis of focusing and contraction in intuitionistic logic

Cited in

(15)

• Maehara-style modal nested calculi
• Non-associative, non-commutative multi-modal linear logic
• A pure view of ecumenical modalities
• Focused proof-search in the logic of bunched implications
• A proof system for fork algebras and its applications to reasoning in logics based on intuitionism
• Focused and Synthetic Nested Sequents
• A semantical analysis of focusing and contraction in intuitionistic logic
• Focused labeled proof systems for modal logic
• Proof search in nested sequent calculi
• Focusing and Polarization in Intuitionistic Logic
• scientific article; zbMATH DE number 6863660 (Why is no real title available?)
• MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
• Canonicity of proofs in constructive modal logic
• The flower calculus
• Separability and harmony in ecumenical systems

This page was built for publication: Modular focused proof systems for intuitionistic modal logics

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