Canonicity of proofs in constructive modal logic

DOI10.1007/978-3-031-43513-3_19MaRDI QIDQ6541161zbMATH OpenFDO

Authors Matteo Acclavio, Davide Catta, Federico Olimpieri

Publication date 17 May 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-43513-3_19

zbMATH Keywords

constructive modal logicgame semanticslambda calculus

Mathematics Subject Classification ID

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

Cites work

• A judgmental reconstruction of modal logic
• A modal analysis of staged computation
• A nonstandard standardization theorem
• A proof calculus which reduces syntactic bureaucracy
• A Theory of Explicit Substitutions with Safe and Full Composition
• Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4
• Call-by-Name and Call-by-Value in Normal Modal Logic
• Closed categories and the theory of proofs
• Combinatorial proofs for constructive modal logic
• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Cut-free Gentzen calculus for multimodal CK
• Dual-context calculi for modal logic
• Focused labeled proof systems for modal logic
• Focussing and proof construction
• Game semantics for constructive modal logic
• scientific article; zbMATH DE number 1670494 (Why is no real title available?)
• scientific article; zbMATH DE number 5852776 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• scientific article; zbMATH DE number 1848312 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3054619 (Why is no real title available?)
• Identity of Proofs Based on Normalization and Generality
• Justification logic for constructive modal logic
• Lectures on the Curry-Howard isomorphism
• Linear logic
• Modal logics for knowledge representation systems
• Modular focused proof systems for intuitionistic modal logics
• Non-wellfounded proof theory for (Kleene+action)(algebras+lattices)
• On full abstraction for PCF: I, II and III
• Proof diagrams for multiplicative linear logic: syntax and semantics
• Proofs without syntax
• Propositional lax logic
• Results on the propositional \(\mu\)-calculus
• The relative efficiency of propositional proof systems
• The Theory of Calculi with Explicit Substitutions Revisited
• The virtues of eta-expansion
• Using branching time temporal logic to synthesize synchronization skeletons

This page was built for publication: Canonicity of proofs in constructive modal logic

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