Analytic Tableaux for Justification Logics
Meghdad Ghari

TL;DR
This paper introduces analytic tableau proof systems for justification logics, demonstrating their soundness, completeness, and decidability, with a focus on syntactic cut elimination and subformula properties.
Contribution
It provides the first tableau systems for justification logics, establishing soundness, completeness, and decidability results with a syntactic proof framework.
Findings
Tableau systems are sound and complete for justification logics.
Decidability is proven for finite constant specifications.
Syntactic cut elimination and subformula property are established.
Abstract
In this paper we present analytic tableau proof systems for various justification logics. We show that the tableau systems are sound and complete with respect to Mkrtychev models. In order to prove the completeness of the tableaux, we give a syntactic proof of cut elimination. We also show the subformula property for our tableaux, and prove the decidability of justification logics for finite constant specifications.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge
