• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computer Science Logic >Open Proofs and Open Terms: A Basis for Interactive Logic
【24h】

Open Proofs and Open Terms: A Basis for Interactive Logic

机译：开放证明和开放术语：交互逻辑的基础

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

摘要

When proving a theorem, one makes intermediate claims, leaving parts temporarily unspecified. These 'open' parts may be proofs but also terms. In interactive theorem proving systems, one prominently deals with these 'unfinished proofs' and 'open terms'. We study these 'open phenomena' from the point of view of logic. This amounts to finding a correctness criterion for 'unfinished proofs' (where some parts may be left open, but the logical steps that have been made are still correct). Furthermore we want to capture the notion of 'proof state'. Proof states are the objects that interactive theorem provers operate on and we want to understand them in terms of logic. In this paper we define 'open higher order predicate logic', an extension of higher order logic with unfinished (open) proofs and open terms. Then we define a type theoretic variant of this open higher order logic together with a formulas-as-types embedding from open higher order logic to this type theory. We show how this type theory nicely captures the notion of 'proof state', which is now a type-theoretic context.
机译：当证明一个定理时，人们会提出中间要求，而暂时不指定部分。这些“开放”部分既可以作为证明，也可以作为术语。在交互式定理证明系统中，一个主要处理这些“未完成的证明”和“公开条款”。我们从逻辑的角度研究这些“开放现象”。这相当于为“未完成的证明”找到正确性标准（其中某些部分可能会保留，但已经执行的逻辑步骤仍然是正确的）。此外，我们想捕捉“证明状态”的概念。证明状态是交互式定理证明者操作的对象，我们希望从逻辑上理解它们。在本文中，我们定义了“开放式高阶谓词逻辑”，它是未完成（开放式）证明和开放式术语的高阶逻辑的扩展。然后，我们定义此开放式高阶逻辑的类型理论变体，以及从开放式高阶逻辑嵌入到该类型理论的按类型填充的公式。我们将展示这种类型理论如何很好地捕捉“证明状态”的概念，该状态现在是类型理论的上下文。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号