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

Gilles Dowek 1 Thérèse Hardin Claude Kirchner 2
2 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.
Type de document :
[Research Report] RR-3556, INRIA. 1998, pp.26
Liste complète des métadonnées

Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 29 mai 2006 - 17:19:26
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : lundi 5 avril 2010 - 21:44:40



  • HAL Id : inria-00077202, version 1


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〉



Consultations de la notice


Téléchargements de fichiers