Hostname: page-component-78c5997874-t5tsf Total loading time: 0 Render date: 2024-11-05T08:44:39.859Z Has data issue: false hasContentIssue false

HOL-λσ: an intentional first-order expression of higher-order logic

Published online by Cambridge University Press:  07 March 2001

GILLES DOWEK
Affiliation:
INRIA-Rocquencourt, B.P. 105, 78153 Le Chesnay Cedex, France Email: [email protected], http://coq.inria.fr/˜dowek
THERESE HARDIN
Affiliation:
LIP6 & INRIA, UPMC, 4 place Jussieu, 75252 Paris Cedex 05, France Email: [email protected], http://www-spi.lip6.fr/˜hardin
CLAUDE KIRCHNER
Affiliation:
LORIA & INRIA, 615, rue du Jardin Botanique, 54600 Villers-lès-Nancy, France Email: [email protected], http://www.loria.fr/˜ckirchne

Abstract

We give a first-order presentation of higher-order logic based on explicit substitutions. This presentation is intentionally equivalent to the usual presentation of higher-order logic based on λ-calculus, that is, a proposition can be proved without the extensionality axioms in one theory if and only if it can be in the other. We show that the Extended Narrowing and Resolution first-order proof-search method can be applied to this theory. In this way we get a step-by-step simulation of higher-order resolution. Hence, expressing higher-order logic as a first-order theory and applying a first-order proof search method is a relevant alternative to a direct implementation. In particular, the well-studied improvements of proof search for first-order logic could be reused at no cost for higher-order automated deduction. Moreover, as we stay in a first-order setting, extensions, such as equational higher-order resolution, may be easier to handle.

Type
Research Article
Copyright
© 2001 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)