Holls: an Intentional First-Order Expression of Higher-Order Logic

2 SPI - Sémantiques, preuves et implantation
LIP6 - Laboratoire d'Informatique de Paris 6
3 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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 $\lambda$-calculus, i.e. a proposition can be proved without the extensionality axioms in one theory if and only if it can in the other. We show that we can apply the \em Extended Narrowing and Resolution first-order proof-search method to this theory. We get this way 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 at least as efficient as a direct implementation. Furthermore, 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, are easier to handle.
Keywords :
Document type :
Reports
Domain :

https://hal.inria.fr/inria-00077202
Contributor : Rapport de Recherche Inria <>
Submitted on : Monday, May 29, 2006 - 5:19:26 PM
Last modification on : Friday, April 10, 2020 - 1:23:35 AM
Long-term archiving on: : Monday, April 5, 2010 - 9:44:40 PM

Identifiers

• HAL Id : inria-00077202, version 1

Citation

Gilles Dowek, Thérèse Hardin, Claude Kirchner. Holls: an Intentional First-Order Expression of Higher-Order Logic. [Research Report] RR-3556, INRIA. 1998, pp.26. ⟨inria-00077202⟩

Record views