在 HOL Light 中捕获分层证明树
计算机科学中的逻辑
2013-07-11 v1
摘要
分层证明树（简称 hiproofs）通过允许树的某些部分进行分层嵌套，为普通证明树增加了结构。这种额外的结构可用于抽象掉细节，或标记特定部分以解释其目的。在本文中，我们提出了两种在 HOL Light 中捕获 hiproofs 的互补方法，以及一个用于生成基于 Web 的可视化的工具。第一种方法使用策略记录（tactic recording），通过修改策略以记录其参数并构建分层树；这使得策略证明脚本可以被修改。第二种方法使用证明记录（proof recording），扩展了 HOL Light 内核以在定理旁记录分层证明树。这种方法侵入性较小，但需要谨慎管理记录对象的大小。我们已实现了这两种方法，形成了两个系统：Tactician 和 HipCam。
引用
@article{arxiv.1307.2713,
title = {Capturing Hiproofs in HOL Light},
author = {Steven Obua and Mark Adams and David Aspinall},
journal= {arXiv preprint arXiv:1307.2713},
year = {2013}
}