Translating Higher-order Clauses to First-Order Clauses

Abstract

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.