Axiomatic and dual systems for constructive necessity, a formally verified equivalence

DOI10.1080/11663081.2019.1647653zbMath1444.03054OpenAlexW2967502375MaRDI QIDQ5231279

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

Publication date: 26 August 2019

Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1080/11663081.2019.1647653

zbMATH Keywords

formal verificationnatural deductionconstructive logicmodal logic S4COQ

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Related Items

A dual-context sequent calculus for the constructive modal logic S4 ⋮ On interactive proof-search for constructive modal necessity ⋮ Dual and axiomatic systems for constructive S4, a formally verified equivalence ⋮ Verification of dynamic bisimulation theorems in Coq

Uses Software

• Coq
• Pesca
• MiniML

Cites Work

• Does the deduction theorem fail for modal logic?
• Natural deduction, hybrid systems and modal logics
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• 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
• Effective completeness theorems for modal logic
• A judgmental reconstruction of modal logic
• Interacting with Modal Logics in the Coq Proof Assistant
• A modal analysis of staged computation
• A Formally Verified Prover for the $\mathcal{ALC\,}$ Description Logic
• The Logic of Proofs as a Foundation for Certifying Mobile Computation
• Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
• A Constructive Presentation for the Modal Connective of Necessity (□)
• Logic in Computer Science
• Why Prove it Again?
• Strict implication, deducibility and the deduction theorem
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item