TY - JOUR
T1 - Translating higher-order clauses to first-order clauses
AU - Meng, Jia
AU - Paulson, Lawrence C.
PY - 2008/1
Y1 - 2008/1
N2 - 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 λ-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.
AB - 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 λ-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.
KW - Clause translation
KW - First-order logic
KW - Higher-order logic
KW - Interactive theorem provers
UR - http://www.scopus.com/inward/record.url?scp=37449033344&partnerID=8YFLogxK
U2 - 10.1007/s10817-007-9085-y
DO - 10.1007/s10817-007-9085-y
M3 - Article
SN - 0168-7433
VL - 40
SP - 35
EP - 60
JO - Journal of Automated Reasoning
JF - Journal of Automated Reasoning
IS - 1
ER -