Labeled sequent calculus for justification logics
Justification logics, emerging from the Logic of Proofs (LP) introduced by \textit{S. N. Artemov} [Bull. Symb. Log. 7, No. 1, 1--36 (2001; Zbl 0980.03059)], are modal-like logics whose language includes formulas of the form $t:A$, meaning ``the term $t$ provides a justification for the truth of the formula $A$. This paper develops calculi for several justification logics: the basic justification logics J corresponding to the modal logics K, its extensions by various combinations of axioms corresponding to the common modal axioms T, D, 4, B, and 5 (including the original logic LP = JT4), and the combined modal-justification logics that extend each of the logics above with an explicit $\square $ operator. \par The calculi provided are labelled sequent calculi in the style of \textit{S. Negri} [J. Philos. Log. 34, No. 5--6, 507--544 (2005; Zbl 1086.03045)], whose language internalizes Kripke-Fitting semantics [\textit{M. Fitting}, Ann. Pure Appl. Logic 132, No. 1, 1--25 (2005; Zbl 1066.03059)] for the logics in question. The author proves admissibility of cut and other structural rules in the calculi, and their completeness. It is shown that some of the calculi are analytical in the sense that they enjoy suitable subformula, subterm, and sublabel properties.
- A syntactic realization theorem for justification logics
- Analytic methods for the logic of proofs
- Conservativity for logics of justified belief: two approaches
- Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
- Cut elimination and realization for epistemic logics with justification
- Cut Elimination in the Presence of Axioms
- Evidence Reconstruction of Epistemic Modal Logic S5
- Explicit provability and constructive semantics
- scientific article; zbMATH DE number 1114348 (Why is no real title available?)
- scientific article; zbMATH DE number 1749009 (Why is no real title available?)
- scientific article; zbMATH DE number 949290 (Why is no real title available?)
- scientific article; zbMATH DE number 6174943 (Why is no real title available?)
- scientific article; zbMATH DE number 6302917 (Why is no real title available?)
- scientific article; zbMATH DE number 2209442 (Why is no real title available?)
- Introducing Justification into Epistemic Logic
- Justification logics, logics of knowledge, and conservativity
- Kripke completeness revisited
- Prefixed tableaus and nested sequents
- Proof Analysis
- Proof analysis in intermediate logics
- Proof analysis in modal logic
- Realization for justification logics via nested sequents: modularity through embedding
- Realization theorems for justification logics: full modularity
- Reasoning about collectively accepted group beliefs
- Tableaux and hypersequents for justification logics
- The logic of justification
- The logic of proofs, semantically
- The ontology of justifications in the logical setting
- Natural deduction and semantic models of justification logic in the proof assistant \textsc{Coq}
- Tableaux and Hypersequents for Justification Logic
- Tableaux and hypersequents for justification logics
- Automated Reasoning with Analytic Tableaux and Related Methods
- The internalized disjunction property for intuitionistic justification logic
- Labeled Sequent Calculus for Orthologic
- On Boolean algebraic structure of proofs: towards an algebraic semantics for the logic of proofs
- Tableaux and interpolation for propositional justification logics
This page was built for publication: Labeled sequent calculus for justification logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q331048)
