Extensional higher-order resolution (Q4249891)

The authors present an extensional higher-order resolution calculus that is complete relative to Henkin model semantics. The core of higher-order resolution is a simple extension of the first-order resolution method to the higher-order language. The only difference is that \(\beta\gamma\)-equality has to be built in by keeping formulae in normal form, and that first-order unification has to be replaced by higher-order unification. Resolution and factorization rules are modified, so that they record the induced unification problem in a unification constraint instead of trying to compute a complete set of unifiers. The calculus is augmented with the inference rules of higher-order unification that are lifted to act on the unification constraint of clauses. Such approach permits to interleave the search for the empty clause and the search for higher-order unifiers and alleviate the undecidability problem. On the basis of a suitable treatment of Leibniz equality, the authors prove that the proposed resolution calculus is sound and complete with respect to Henkin's general model semantics. For the entire collection see [Zbl 0892.00047].