Logic Journal of the IGPL (forthcoming)
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 |
![]() ![]() ![]() ![]() |
Download options
References found in this work BETA
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.
Multi-Agent Justification Logic: Communication and Evidence Elimination. [REVIEW]Bryan Renne - 2012 - Synthese 185 (S1):43-82.
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.
Similar books and articles
Inference as Doxastic Agency. Part II: Ramifications and Refinements.Heinrich Wansing & Grigory K. Olkhovikov - 2017 - Australasian Journal of Logic 14 (4):408-438.
Proof-Theoretic Semantic Values for Logical Operators.Nissim Francez & Gilad Ben-avi - 2011 - Review of Symbolic Logic 4 (3):466-478.
Natural Deduction: A Proof-Theoretical Study.Dag Prawitz - 1965 - Stockholm, Sweden: Dover Publications.
The Ontology of Justifications in the Logical Setting.Sergei N. Artemov - 2012 - Studia Logica 100 (1-2):17-30.
Commentary and Illocutionary Expressions in Linear Calculi of Natural Deduction.Moritz Cordes & Friedrich Reinmuth - 2017 - Logic and Logical Philosophy 26 (2).
Natural Deduction for Non-Classical Logics.David Basin, Seán Matthews & Luca Viganò - 1998 - Studia Logica 60 (1):119-160.
Harmony in Multiple-Conclusion Natural-Deduction.Nissim Francez - 2014 - Logica Universalis 8 (2):215-259.
Justifications, Awareness and Epistemic Dynamics.Igor Sedlár - 2013 - In Sergei Artemov & Anil Nerode (eds.), Logical Foundations of Computer Science (Lecture Notes in Computer Science 7734). Springer. pp. 307-318.
A Labelled Deduction System for Kanger's Theory of Rights.Berislav Žarnić - 2006 - Filozofska Istrazivanja 26 (3):731-755.
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.
The Deduction Rule and Linear and Near-Linear Proof Simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - Journal of Symbolic Logic 58 (2):688-709.
Axiomatic and Dual Systems for Constructive Necessity, a Formally Verified Equivalence.Lourdes del Carmen González-Huesca, Favio E. Miranda-Perea & P. Selene Linares-Arévalo - 2019 - Journal of Applied Non-Classical Logics 29 (3):255-287.
Analytics
Added to PP index
2020-06-26
Total views
18 ( #608,386 of 2,507,392 )
Recent downloads (6 months)
2 ( #277,263 of 2,507,392 )
2020-06-26
Total views
18 ( #608,386 of 2,507,392 )
Recent downloads (6 months)
2 ( #277,263 of 2,507,392 )
How can I increase my downloads?
Downloads