Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4

DOI10.1007/978-3-540-73595-3_9MaRDI QIDQ3608769zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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; zbMATH DE number 1189111

Cited in

(7)

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

Describes a project that uses

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)