【24h】

Proof Theory Corner

机译:证明理论角

获取原文
获取原文并翻译 | 示例
           

摘要

The Proof Theory Corner is devoted to all papers related to the areas of proof theory and automated reasoning, with a particular emphasis on formal systems for logics and theories which have computational aspects or are significant for the foundations of mathematics.rnIn this issue, Luca Alberucci presents an article entitled 'Sequent Calculi for the modal μ-Calculus over S5'. Modal mu-calculus is modal logic with fixed points. The paper addresses the issue of a (sound and) complete proof system for S5 modal mu-calculus, when the transition relation is an equivalence relation. Semantically this means that the distance between states along the transition relation is bounded by two and that therefore the logic collapses into its modal fragment: a fixed point will be reached by approximant level two. Here, the author shows that this can also be done syntactically, thereby providing a simple sound and complete Tait-type proof system for the logic.
机译:证明论角专门用于与证明论和自动推理领域有关的所有论文,尤其着重于逻辑和理论的形式系统,这些逻辑和理论具有计算方面的意义或对数学的基础具有重要意义。在本期中,卢卡·阿尔贝鲁奇(Luca Alberucci)提出了一篇题为“ S5上的模态微积分的后续计算”的文章。模态微积分是具有固定点的模态逻辑。当过渡关系是等价关系时,本文讨论了S5模态微积分的(完整的)证明系统的问题。从语义上讲,这意味着沿过渡关系的状态之间的距离为2限制,因此逻辑崩溃为它的模态片段:一个固定点将达到近似2级。在这里,作者表明这也可以在语法上完成,从而为逻辑提供了一个简单的声音和完整的Tait型证明系统。

著录项

  • 来源
    《Journal of logic and computation》 |2009年第6期|969|共1页
  • 作者

    Arnon Avron;

  • 作者单位

    School of Computer Science, Tel-Aviv University, Tel-Aviv, Israel;

  • 收录信息
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号