• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >Unified Semantics and Proof System for Classical, Intuitionistic and Affine Logics
【24h】

Unified Semantics and Proof System for Classical, Intuitionistic and Affine Logics

机译：古典，直觉和仿射逻辑的统一语义和证明系统

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This paper modifies our previous work in combining classical logic with intuitionistic logic [16], [17] to also include affine linear logic, resulting in a system we call Affine Control Logic. A propositional system with six binary connectives is defined and given a phase space interpretation. Choosing classical, intuitionistic or affine reasoning is entirely dependent on the subformula property. Moreover, the connectives of these logics can mix without restriction. We give a sound and complete sequent calculus that requires novel proof transformations for cut elimination. Compared to linear logic, classical fragments of proofs are better isolated from non-classical fragments. One of our goals is to allow non-classical restrictions to coexist with computational interpretations of classical logic such as found in the λμ calculus. In fact, we show that the transition between different modes of proof, classical, intuitionistic and affine, can be interpreted by delimited control operators. We also discuss how to extend the definition of focused proofs to this logic.
机译：本文修改了我们先前的工作，将经典逻辑与直觉逻辑[16] [17]结合起来，还包括仿射线性逻辑，从而形成了一个称为仿射控制逻辑的系统。定义了具有六个二元连接词的命题系统，并给出了相空间解释。选择经典，直觉或仿射推理完全取决于子公式的属性。而且，这些逻辑的连接词可以不受限制地混合。我们给出完整而完整的演算，需要新颖的证明变换来消除割痕。与线性逻辑相比，经典的证明片段可以更好地与非经典的片段隔离。我们的目标之一是让非经典限制与经典逻辑的计算解释（例如λμ演算中）共存。实际上，我们证明了不同的证明模式（经典，直觉和仿射）之间的过渡可以由定界控制算子解释。我们还将讨论如何将重点证明的定义扩展到此逻辑。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号