Translating Higher-order Clauses to First-Order Clauses
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...[Show more]
|Collections||ANU Research Publications|
|Source:||Journal of Automated Reasoning|
|01_Paulson_Translating_Higher-order_2008.pdf||322.66 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.