Paulson, Lawrence C.Meng, Jia2015-12-100168-7433http://hdl.handle.net/1885/51458Interactive 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.Keywords: Abstracting; Function evaluation; Interactive computer systems; Logic programming; Clause translation; Higher order logic; Interactive theorem provers; Theorem proving Clause translation; First-order logic; Higher-order logic; Interactive theorem provers200810.1007/s10817-007-9085-y2015-12-09