• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International workshop on 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.
机译：当证明定理时，一个人犯下中间权利要求，暂时未指明的零件。这些“开放”部件可能是证明还可以是术语。在互动定理证明系统中，一个突出地涉及这些“未完成的证据”和“开放条款”。我们从逻辑的角度来研究这些“开放现象”。这增加了为“未完成的证据”找到正确的标准（某些部件可能留下开放，但所做的逻辑步骤仍然是正确的）。此外，我们希望捕捉“校对状态”的概念。证明状态是互动定理普通操作的对象，我们希望在逻辑方面了解它们。在本文中，我们定义了“开放高阶谓词逻辑”，扩展了更高阶逻辑，未完成（打开）校样和开放项。然后，我们将此开放的高阶逻辑的类型定理变体与嵌入到这种类型理论的公开阶逻辑嵌入的公式 - AS型逻辑。我们展示了这种类型的理论如何很好地捕获“校对状态”的概念，现在是一个理论上的上下文。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号