Natural deduction and semantic models of justification logic in the proof assistant \textsc{Coq}

DOI10.1093/JIGPAL/JZAA007MaRDI QIDQ3386915zbMATH OpenOpenAlexFDO

Authors Jesús Mauricio Andrade Guzmán, Francisco Hernández-Quiroz

Publication date 8 January 2021

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/jigpal/jzaa007

zbMATH Keywords

\textsc{Coq}justification logicmodal logicnatural deductionsoundness

Mathematics Subject Classification ID

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

Recommendations

• Justification logic. Reasoning with reasons
• The first-order hypothetical logic of proofs
• The ontology of justifications in the logical setting
• Logics of proofs and justifications
• Labeled sequent calculus for justification logics

Cited in

(6)

• The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
• Natural language inference in Coq
• A Curry-Howard view of basic justification logic
• Interacting with Modal Logics in the Coq Proof Assistant
• Axiomatic and dual systems for constructive necessity, a formally verified equivalence
• \textsf{LOGIC}: a Coq library for logics

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Natural deduction and semantic models of justification logic in the proof assistant \textsc{Coq}

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