Natural deduction and semantic models of justification logic in the proof assistant Coq

Logic Journal of the IGPL (forthcoming)
  Copy   BIBTEX


The purpose of this paper is to present a formalization of the language, semantics and axiomatization of justification logic in Coq. We present proofs in a natural deduction style derived from the axiomatic approach of justification logic. Additionally, we present possible world semantics in Coq based on Fitting models to formalize the semantic satisfaction of formulas. As an important result, with this implementation, it is possible to give a proof of soundness for $\mathsf{L}\mathsf{P}$ with respect to Fitting models.



    Upload a copy of this work     Papers currently archived: 83,802

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Free Semantics.Ross Thomas Brady - 2010 - Journal of Philosophical Logic 39 (5):511 - 529.
Natural deduction: a proof-theoretical study.Dag Prawitz - 1965 - Mineola, N.Y.: Dover Publications.
Harmony in Multiple-Conclusion Natural-Deduction.Nissim Francez - 2014 - Logica Universalis 8 (2):215-259.
Labeled sequent calculus for justification logics.Meghdad Ghari - 2017 - Annals of Pure and Applied Logic 168 (1):72-111.
Natural Deduction for Modal Logic with a Backtracking Operator.Jonathan Payne - 2015 - Journal of Philosophical Logic 44 (3):237-258.


Added to PP

23 (#530,329)

6 months
2 (#323,023)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

No citations found.

Add more citations

References found in this work

Explicit provability and constructive semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
The logic of justification.Sergei Artemov - 2008 - Review of Symbolic Logic 1 (4):477-513.
The logic of proofs, semantically.Melvin Fitting - 2005 - Annals of Pure and Applied Logic 132 (1):1-25.
Pavelka-style fuzzy justification logics.Meghdad Ghari - 2016 - Logic Journal of the IGPL 24 (5):743-773.

View all 6 references / Add more references