Extensional higher-order resolution
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].
- Comparing approaches to resolution based higher-order theorem proving
- scientific article; zbMATH DE number 5595970 (Why is no real title available?)
- Extensional higher-order paramodulation and RUE-resolution
- Higher-Order Multi-Valued Resolution
- Higher-order semantics and extensionality
- Set-of-support strategy for higher-order logic
- Superposition with lambdas
- Superposition with lambdas
- SAT-Inspired Higher-Order Eliminations
- HoCHC: a refutationally complete and semantically invariant system of higher-order logic modulo theories
- Types, Tableaus and Gödel’s God in Isabelle/HOL
This page was built for publication: Extensional higher-order resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4249891)
