Authors
Abstract
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.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1093/jigpal/jzaa007
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 50,488
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

The Logic of Justification.Sergei Artemov - 2008 - Review of Symbolic Logic 1 (4):477-513.
Explicit Provability and Constructive Semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
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

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Free Semantics.Ross Thomas Brady - 2010 - Journal of Philosophical Logic 39 (5):511 - 529.
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.

Analytics

Added to PP index
2020-06-26

Total views
6 ( #1,025,621 of 2,326,762 )

Recent downloads (6 months)
6 ( #128,611 of 2,326,762 )

How can I increase my downloads?

Downloads

My notes