• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of Symbolic Logic >Strong cut-elimination in sequent calculus using Klop's l-translation and perpetual reductions
【24h】

Strong cut-elimination in sequent calculus using Klop's l-translation and perpetual reductions

机译：使用克洛普（Klop）的l平移和永续归约法在后续演算中进行强切除

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

摘要

There is a simple technique. due to Dragalin, for proving strong cut-elimination for intuitionistic sequent calculus, but the technique is constrained to certain choices of reduction rules. preventing equally natural alternatives. We consider such a natural. alternative set of reduction rules and show that the classical technique is inapplicable. Instead we develop another approach combining two of our favorite tools-Klop's l-translation and perpetual reductions. These tools are of independent interest and have proved useful in a variety of settings: it is therefore natural to investigate, as we do here, what they have to offer the field of sequent calculus.
机译：有一个简单的技术。由于德拉加林（Dragalin）的缘故，它证明了直觉式后续演算的强切消法，但该技术仅限于约简规则的某些选择。防止同样自然的选择。我们认为这很自然。约简规则的替代集，并表明经典技术不适用。相反，我们开发了另一种方法，将我们最喜欢的两种工具结合在一起：Klop的l翻译和永久减少。这些工具具有独立的意义，并已证明在多种环境中有用：因此，像我们在这里所做的那样，自然地研究它们为后续演算领域提供了哪些工具是很自然的。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号