Holls: an Intentional First-Order Expression of Higher-Order Logic
Résumé
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.