Embedding constructive K into intuitionistic K

DOI10.1016/J.ENTCS.2010.04.015MaRDI QIDQ3185769zbMATH OpenOpenAlexFDO

Authors Kurt Ranalter

Publication date 5 August 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2010.04.015

zbMATH Keywords

constructive modal logicextended natural deduction systemsintuitionistic modal logicpossibility

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Proof theory in general (including proof-theoretic semantics) (03F03)

Recommendations

• scientific article; zbMATH DE number 1612552
• Constructive embedding from extensions of logics of strict implication into modal logics
• On nested sequents for constructive modal logics
• scientific article; zbMATH DE number 7599983
• One-step modal logics, intuitionistic and classical. I

Cites work

• A judgmental reconstruction of modal logic
• A modal analysis of staged computation
• Computational types from a logical perspective
• scientific article; zbMATH DE number 5360220 (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?)
• Intuitionistic hybrid logic
• Natural deduction and context as (constructive) modality
• Notions of computation and monads
• Proof analysis in modal logic
• Propositional lax logic
• Symbolic Representations of the Post-apartheid University
• Towards constructive DL for abstraction and refinement

Cited in

(6)

• Basic intuitionistic conditional logic
• scientific article; zbMATH DE number 1612552 (Why is no real title available?)
• Constructive description logics hybrid-style
• Constructive embedding from extensions of logics of strict implication into modal logics
• Logic of intuitionistic interactive proofs (formal theory of perfect knowledge transfer)
• Cut-free Gentzen calculus for multimodal CK

Describes a project that uses

Uses Software

• MiniML

This page was built for publication: Embedding constructive K into intuitionistic K

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