Labeled sequent calculus for justification logics
| Autor: | Meghdad Ghari |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Soundness
Discrete mathematics Natural deduction Logic Cut-elimination theorem 010102 general mathematics Noncommutative logic Modal logic Sequent calculus 0102 computer and information sciences 01 natural sciences law.invention TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Invertible matrix 010201 computation theory & mathematics law TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Calculus Sequent 0101 mathematics Mathematics |
| Zdroj: | Annals of Pure and Applied Logic. 168:72-111 |
| ISSN: | 0168-0072 |
| Popis: | Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modal-justification logics. Using a method due to Sara Negri, we internalize the Kripke-style semantics of justification and modal-justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (weakening and contraction) and the cut rule are admissible. Soundness and completeness are established as well. The analyticity for some of our labeled sequent calculi are shown by proving that they enjoy the subformula, sublabel and subterm properties. We also present an analytic labeled sequent calculus for S4LPN based on Artemov–Fitting models. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect