• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Cut Elimination and Realization for Epistemic Logics with Justification
【24h】

Cut Elimination and Realization for Epistemic Logics with Justification

机译：有理有据地削减和消除认知逻辑

获取原文
获取原文并翻译 | 示例
       
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Epistemic logics with justification, S4LP and S4LPN, are combinations of the modal epistemic logic S4 and the Logic of Proofs LP, with some connecting principles. These logics together with the modal knowledge operator OF (F is known), contain infinitely many operators of the form t: F (t is a justification for F), where Ms a term. Regarding the Realization Theorem of S4, LP is the justification counterpart of S4, in the sense that, every theorem of S4 can be transformed into a theorem of LP (by replacing all occurrences of □ by suitable terms), and vise versa. In this article, we first introduce a new cut-free sequent calculus LP_L~G for LP, and then extend it to obtain a cut-free sequent calculus for S4LP and a cut-free hypersequent calculus for S4LPN. All cut elimination theorems are proved syntactically. Moreover, these sequent systems enjoy a weak subformula property. Then, we show that theorems of S4LP can be realized in LP and theorems of S4LPN can be realized in JS5 (the justification counterpart of modal logic S5). Consequently, we prove that S4LP and S4LPN are conservative extensions of LP.
机译：有理由的认知逻辑S4LP和S4LPN是模态认知逻辑S4和证明逻辑LP的组合，具有一些连接原理。这些逻辑与模态知识运算符OF（F是已知的）一起包含无限多种形式为t：F（t是F的称谓）的运算符，其中Ms是项。关于S4的实现定理，从S4的每个定理都可以转化为LP定理（通过用适当的术语替换□的所有出现）的意义上讲，LP是S4的证明对等物。在本文中，我们首先为LP引入了一种新的免割后续演算LP_L〜G，然后对其进行扩展，以获得S4LP的免割后续演算和S4LPN的免割超后续演算。所有割消除定理都在语法上得到证明。此外，这些后续系统具有弱的子公式属性。然后，我们证明S4LP的定理可以在LP中实现，而S4LPN的定理可以在JS5（模态逻辑S5的对等匹配）中实现。因此，我们证明S4LP和S4LPN是LP的保守扩展。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号