Cut-free Gentzen calculus for multimodal CK

DOI10.1016/J.IC.2011.10.003zbMATH Open1248.03036OpenAlexW2020894459MaRDI QIDQ764259FDOQ764259

Authors: Michael Mendler, Stephan Scheele 

Publication date: 13 March 2012

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2011.10.003

Recommendations

• Cut-free modal sequents for normal modal logics
• Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom
• On nested sequents for constructive modal logics
• scientific article; zbMATH DE number 1252393
• Sequent Calculi for Multi-modal Logic with Interaction

zbMATH Keywords

Curry-Howard correspondencecut eliminationsequent calculusconstructive modal logic

Mathematics Subject Classification ID

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

Cites Work

• Many-dimensional modal logics: theory and applications
• A judgmental reconstruction of modal logic
• Title not available (Why is that?)
• The Description Logic Handbook
• Notions of computation and monads
• A modal analysis of staged computation
• Monad as modality
• Title not available (Why is that?)
• Propositional lax logic
• Tableaux for constructive concurrent dynamic logic
• An intuitiomstic completeness theorem for intuitionistic predicate logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Computer Science Logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Computational types from a logical perspective
• Title not available (Why is that?)
• Topological duality for intuitionistic modal algebras
• Title not available (Why is that?)
• Constructive modal logics. I
• Title not available (Why is that?)
• 2-sequent calculus: A proof theory of modalities
• Recursion over objects of functional type
• Title not available (Why is that?)
• Embedding Constructive K into Intuitionistic K
• Extending the Curry-Howard interpretation to linear, relevant and other resource logics
• 2-Sequent Calculus: Intuitionism and Natural Deduction
• A computational formalization for partial evaluation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Towards constructive DL for abstraction and refinement

Cited In (8)

• Maehara-style modal nested calculi
• The Došen square under construction: a tale of four modalities
• Terminating calculi and countermodels for constructive modal logics
• Intuitionistic non-normal modal logics: a general framework
• Correspondence theory for modal Fairtlough-Mendler semantics of intuitionistic modal logic
• Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom
• Game semantics for constructive modal logic
• Canonicity of proofs in constructive modal logic

Uses Software

• MiniML

This page was built for publication: Cut-free Gentzen calculus for multimodal CK

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