Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4

DOI10.1007/978-3-540-73595-3_9zbMATH Open1213.03029OpenAlexW2114469058MaRDI QIDQ3608769FDOQ3608769

Authors: Samuli Heilala, Brigitte Pientka 

Publication date: 6 March 2009

Published in: Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73595-3_9

Recommendations

• Tree-sequent calculi and decision procedures for intuitionistic modal logics
• On sequent calculi for intuitionistic propositional logic.
• Label-free proof systems for intuitionistic modal logic IS5
• On an intuitionistic modal logic
• scientific article

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Cited In (6)

• A dual-context sequent calculus for the constructive modal logic S4
• On interactive proof-search for constructive modal necessity
• Intuitionistic non-normal modal logics: a general framework
• Game semantics for constructive modal logic
• Canonicity of proofs in constructive modal logic
• Harpoon: mechanizing metatheory interactively

Uses Software

• ILTP

This page was built for publication: Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4

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