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

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, i.e. a proposition can be proved without the extensionality axioms in one theory if and only if it can in the other. Applying the Extended Narrowing and Resolution proof-search method to this theory simulates higher-order resolution step by step. Hence expressing higher-order logic as a first-order theory and applying a first-order proof search method does not necessarily lead to inefficiencies. As we stay in a first-order setting, extensions, such as equational higher-order resolution, are easier to handle