Translating Higher-Order Clauses to First-Order Clauses

Interactive provers typically use higher-order logic, while automatic provers typically use first-order logic. In order to integrate interactive provers with automatic ones, it is necessary to translate higher-order formulae 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.

• Type: Journal
• Year: 2008
• Where: JAR
• Authors: Jia Meng, Lawrence C. Paulson
• Keywords: Automatic Provers, Interactive Prover, JAR 2008, Success Rates