Source-Level Proof Reconstruction for Interactive Theorem Proving
Source-Level Proof Reconstruction for Interactive Theorem Proving
复制标题
交互式定理证明的源级证明重构
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Kong Woei Susanto
中科院分区：
文献类型：
--
作者：
Lawrence Charles Paulson;Kong Woei Susanto
交互式证明助理应该验证他们从自动定理证明器收到的证明。通常，这种证明重建在内部进行，形成两个工具之间集成的一部分。我们已经实现了源代码级的证明重建：分辨率证明自动转换为Isabelle证明脚本。用户可以将此文本插入到他们的校样开发或（如果他们愿意）手动检查它。证明的每一步都是通过调用Hurd的Metis证明器来证明的，我们已经将其移植到Isabelle。这个项目中一个经常出现的问题是Isabelle的公理类型类的处理。
Interactive proof assistants should verify the proofs they receive from automatic theorem provers. Normally this proof reconstruction takes place internally, forming part of the integration between the two tools. We have implemented source-level proof reconstruction: resolution proofs are automatically translated to Isabelle proof scripts. Users can insert this text into their proof development or (if they wish) examine it manually. Each step of a proof is justified by calling Hurd's Metis prover, which we have ported to Isabelle. A recurrent issue in this project is the treatment of Isabelle's axiomatic type classes.
高阶逻辑中的定理证明
DOI：
10.1007/978-3-540-71067-7_8
发表时间：
2008
期刊：
--
影响因子：
--
作者：
Aehlig K
通讯作者：
Aehlig K