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.
Higher Order Unification via Explicit Substitutions
