Skip navigation
Skip navigation

Translating Higher-order Clauses to First-Order Clauses

Paulson, Lawrence C.; Meng, Jia


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]

CollectionsANU Research Publications
Date published: 2008
Type: Journal article
Source: Journal of Automated Reasoning
DOI: 10.1007/s10817-007-9085-y


File Description SizeFormat Image
01_Paulson_Translating_Higher-order_2008.pdf322.66 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator