• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Completeness and Cut-elimination in the Intuitionistic Theory of Types
【24h】

Completeness and Cut-elimination in the Intuitionistic Theory of Types

机译：直觉类型理论中的完备与删节

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

摘要

In this paper we define a model theory and give a semantic proof of cut-elimination for ICTT, an intuitionistic formulation of Church's theory of types defined by Miller et. al. and the basis for the λProlog programming language. Our approach, extending techniques of Takahashi and Andrews and tableaux machinery of Fitting, Smullyan, Nerode and Shore, is to prove a completeness theorem for the cut-free fragment and show semantically that cut is a derived rule. This allows us to generalize a result of Takahashi and Schuette on extending partial truth valuations in impredicative systems. We extend Andrews' notion of Hintikka sets to intuitionistic higher-order logic in a way that also defines tableau-provability for intuitionistic type theory. In addition to giving a completeness theorem without using cut we then show, using cut, how to establish completeness of more conventional term models. These models give a declarative semantips for the logic underlying the λProlog programming language.
机译：在本文中，我们定义了一个模型理论，并给出了ICTT消减的语义证明，这是Miller等人定义的丘奇类型理论的直觉表述。等以及λProlog编程语言的基础。我们的方法，扩展了Takahashi和Andrews的技术，以及Fitting，Smullyan，Nerode和Shore的tableaux机器，证明了无割片段的完备性定理，并从语义上证明了割是一个衍生规则。这使我们可以概括高桥和舒特在定律系统中扩展部分真值评估的结果。我们将安德鲁斯（Andrews）的Hintikka集的概念扩展到直觉的高阶逻辑，该方式还定义了直觉类型理论的表可证明性。除了给出不使用割的完备性定理外，我们还使用割来展示如何建立更常规术语模型的完整性。这些模型为λProlog编程语言的基本逻辑提供了声明性的技巧。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号