zbMATH — the first resource for mathematics

HOL-$$\lambda\sigma$$: An intentional first-order expression of higher-order logic. (English) Zbl 0972.03012
Summary: 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)
Full Text: