Translating Higher-order Clauses to First-Order Clauses

Date

2008

Authors

Paulson, Lawrence C.
Meng, Jia

Journal Title

Journal ISSN

Volume Title

Publisher

Kluwer Academic Publishers

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.

Description

Keywords

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 provers

Citation

Source

Journal of Automated Reasoning

Type

Journal article

Book Title

Entity type

Access Statement

License Rights

DOI

10.1007/s10817-007-9085-y

Restricted until

2037-12-31