Tableaux and hypersequents for justification logics
- 作者：Hidenori Kurokawa hkurokawa@gc.cuny.edu
- 关键词：03B45 ; 03B62 ; 03F05
- 刊名：Annals of Pure and Applied Logic
- 出版年：2012
- 期刊代码：4_01680072
- 类别：cp
- 出版时间：July, 2012
- 卷：163
- 期：7
- 页码：831-853
- 文件大小：360 K
摘要
Justification logic is a new generation of epistemic logics which along with the traditional modal knowledge/belief operators also consider justification assertions 鈥?is a justification for .鈥?In this paper, we introduce a prefixed tableau system for one of the major logics of this kind S4LPN, which combines the Logic of Proofs (LP) and epistemic logic S4 with an explicit negative introspection principle . We show that the prefixed tableau system for S4LPN is sound and complete with respect to Fitting-style semantics. We also introduce a hypersequent calculus HS4LPN and show that HS4LPN is complete. We establish this fact by using a translation from the prefixed tableau system to the hypersequent calculus. This completeness result gives us a semantic proof of cut-admissibility for S4LPN. We conclude the paper by discussing a subsystems of S4LPN, namely S4LP.