• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Intelligent computer mathematics >Capturing Hiproofs in HOL Light
【24h】

Capturing Hiproofs in HOL Light

机译：在HOL灯光下捕捉Hiproof

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

摘要

Hierarchical proof trees (hiproofs for short) add structure to ordinary proof trees, by allowing portions of trees to be hierarchically nested. The additional structure can be used to abstract away from details, or to label particular portions to explain their purpose. In this paper we present two complementary methods for capturing hiproofs in HOL Light, along with a tool to produce web-based visualisations. The first method uses tactic recording, by modifying tactics to record their arguments and construct a hierarchical tree; this allows a tactic proof script to be modified. The second method uses proof recording, which extends the HOL Light kernel to record hierachical proof trees alongside theorems. This method is less invasive, but requires care to manage the size of the recorded objects. We have implemented both methods, resulting in two systems: Tactician and HipCam.
机译：分层证明树（简称Hiproof）通过允许部分树被嵌套来为普通证明树添加结构。附加结构可用于抽象化细节，或标记特定部分以解释其目的。在本文中，我们介绍了两种在HOL Light中捕获高保真度的互补方法，以及一种用于生成基于Web的可视化效果的工具。第一种方法是使用战术记录，方法是修改战术以记录其参数并构建层次树。这允许修改战术证明脚本。第二种方法使用证明记录，它扩展了HOL Light内核以在定理旁边记录层次证明树。该方法侵入性较小，但需要注意管理记录对象的大小。我们已经实现了这两种方法，因此产生了两个系统：Tactician和HipCam。

著录项

  • 来源
    《Intelligent computer mathematics》|2013年|184-199|共16页
  • 会议地点 Bath(GB)
  • 作者

    Steven Obua; Mark Adams; David Aspinall;

  • 作者单位

    School of Informatics, University of Edinburgh;

    School of Informatics, University of Edinburgh;

    School of Informatics, University of Edinburgh;

  • 会议组织
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号