HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic.

*(English)*Zbl 0972.03012Summary: 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, 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.

##### MSC:

03B35 | Mechanization of proofs and logical operations |

03B15 | Higher-order logic; type theory (MSC2010) |

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |