Cut-free Gentzen calculus for multimodal CK

DOI10.1016/J.IC.2011.10.003MaRDI QIDQ764259zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 2185713 (Why is no real title available?)
• scientific article; zbMATH DE number 3668566 (Why is no real title available?)
• scientific article; zbMATH DE number 192927 (Why is no real title available?)
• scientific article; zbMATH DE number 1231474 (Why is no real title available?)
• scientific article; zbMATH DE number 1028819 (Why is no real title available?)
• scientific article; zbMATH DE number 1042221 (Why is no real title available?)
• scientific article; zbMATH DE number 1078585 (Why is no real title available?)
• scientific article; zbMATH DE number 2064301 (Why is no real title available?)
• scientific article; zbMATH DE number 2085167 (Why is no real title available?)
• scientific article; zbMATH DE number 1848312 (Why is no real title available?)
• scientific article; zbMATH DE number 970633 (Why is no real title available?)
• scientific article; zbMATH DE number 3054619 (Why is no real title available?)
• 2-Sequent Calculus: Intuitionism and Natural Deduction
• 2-sequent calculus: A proof theory of modalities
• A computational formalization for partial evaluation
• A judgmental reconstruction of modal logic
• A modal analysis of staged computation
• An intuitiomstic completeness theorem for intuitionistic predicate logic
• Computational types from a logical perspective
• Computer Science Logic
• Constructive modal logics. I
• Embedding constructive K into intuitionistic K
• Extending the Curry-Howard interpretation to linear, relevant and other resource logics
• Many-dimensional modal logics: theory and applications
• Monad as modality
• Notions of computation and monads
• Propositional lax logic
• Recursion over objects of functional type
• Tableaux for constructive concurrent dynamic logic
• The Description Logic Handbook
• Topological duality for intuitionistic modal algebras
• Towards constructive DL for abstraction and refinement

Cited in

(9)

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

Describes a project that uses

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)