Translating higher-order clauses to first-order clauses
Translating higher-order clauses to first-order clauses
复制标题
DOI：
10.1007/s10817-007-9085-y
复制
发表时间：
2008-01-01
期刊：
影响因子：
--
通讯作者：
Paulson, Lawrence C.
中科院分区：
文献类型：
--
作者：
Meng, Jia;Paulson, Lawrence C.
交互式证明器通常使用高阶逻辑，而自动证明器通常使用一阶逻辑。为了集成交互式证明器与自动证明器，必须将高阶公式转换为一阶形式。理想情况下，翻译应该既合理又实用。我们已经研究了几种转换函数应用程序、类型和抽象的方法。省略一些类型信息可以提高成功率，但可能是不可靠的，因此交互式证明器必须验证证明。本文提出了实验数据，比较翻译的成功率为三个自动证明。
Interactive provers typically use higher-order logic, while automatic provers typically use first-order logic. To integrate interactive provers with automatic ones, one must translate higher-order formulas to first-order form. The translation should ideally be both sound and practical. We have investigated several methods of translating function applications, types, and lambda-abstractions. Omitting some type information improves the success rate but can be unsound, so the interactive prover must verify the proofs. This paper presents experimental data that compares the translations in respect of their success rates for three automatic provers.