Labeled Sequent Calculus and Countermodel Construction for Justification Logics
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2014
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866915104739557376 |
|---|---|
| author | Ghari, Meghdad |
| author_facet | Ghari, Meghdad |
| contents | 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 hybrid modal-justification logics. Using the method due to Sara Negri, we internalize the Kripke-style semantics of justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculus. We show that our labeled sequent calculi enjoy a weak subformula property, all of the rules are invertible and the structural rules (weakening and contraction) and cut are admissible. Finally soundness and completeness are established, and termination of proof search for some of the labeled systems are shown. We describe a procedure, for some of the labeled systems, which produces a derivation for valid sequents and a countermodel for non-valid sequents. We also show a model correspondence for justification logics in the context of labeled sequent calculus. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1401_1065 |
| institution | arXiv |
| publishDate | 2014 |
| record_format | arxiv |
| spellingShingle | Labeled Sequent Calculus and Countermodel Construction for Justification Logics Ghari, Meghdad Logic Logic in Computer Science 03B45, 03B60, 03F05 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 hybrid modal-justification logics. Using the method due to Sara Negri, we internalize the Kripke-style semantics of justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculus. We show that our labeled sequent calculi enjoy a weak subformula property, all of the rules are invertible and the structural rules (weakening and contraction) and cut are admissible. Finally soundness and completeness are established, and termination of proof search for some of the labeled systems are shown. We describe a procedure, for some of the labeled systems, which produces a derivation for valid sequents and a countermodel for non-valid sequents. We also show a model correspondence for justification logics in the context of labeled sequent calculus. |
| title | Labeled Sequent Calculus and Countermodel Construction for Justification Logics |
| topic | Logic Logic in Computer Science 03B45, 03B60, 03F05 |
| url | https://arxiv.org/abs/1401.1065 |