Cut-free Gentzen calculus for multimodal CK

DOI10.1016/j.ic.2011.10.003zbMath1248.03036MaRDI QIDQ764259

Stephan Scheele, Michael Mendler

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

cut elimination; sequent calculus; Curry-Howard correspondence; constructive modal logic

Mathematics Subject Classification ID

03B45: Modal logic (including the logic of norms)

03F05: Cut-elimination and normal-form theorems

Related Items

Intuitionistic non-normal modal logics: a general framework, Maehara-style modal nested calculi, Terminating calculi and countermodels for constructive modal logics, Game semantics for constructive modal logic, The Došen square under construction: a tale of four modalities

Uses Software

• MiniML

Cites Work

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