Dual and axiomatic systems for constructive S4, a formally verified equivalence

DOI10.1016/j.entcs.2020.02.005zbMath1495.03032OpenAlexW3013261218WikidataQ113317342 ScholiaQ113317342MaRDI QIDQ2219076

Favio E. Miranda-Perea, P. Selene Linares-Arévalo, Lourdes del Carmen González Huesca

Publication date: 19 January 2021

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

zbMATH Keywords

formal verificationnatural deductionconstructive logicCoqmodal logic S4dual calculus

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

A dual-context sequent calculus for the constructive modal logic S4

Uses Software

• Coq
• MiniML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Does the deduction theorem fail for modal logic?
• Natural deduction, hybrid systems and modal logics
• Lectures on the Curry-Howard isomorphism
• Gentzen calculi for modal propositional logic
• Proof methods for modal and intuitionistic logics
• Propositional lax logic
• Monad as modality
• Encoding modal logics in logical frameworks
• Fitch-style modal lambda calculi
• A judgmental reconstruction of modal logic
• A modal analysis of staged computation
• The Logic of Proofs as a Foundation for Certifying Mobile Computation
• A Constructive Presentation for the Modal Connective of Necessity (□)
• Multi-Agent Dialogues and Dialogue Sequents for Proof Search and Scheduling in Intuitionistic Logic and the Modal Logic S4
• Logic in Computer Science
• Axiomatic and dual systems for constructive necessity, a formally verified equivalence

This page was built for publication: Dual and axiomatic systems for constructive S4, a formally verified equivalence