Henkin Completeness of Higher-Order Resolution
Christoph Benzmüller, Michael Kohlhase · 1999
In this paper we present an extensional higher-order resolution calculus that is complete relative to Henkin model semantics. The treatment of the extensionality principles -- necessary for the completeness result -- by specialized (goal-directed) inference rules is of practical applicability, as an implentation of the calculus in the Leo-System shows. Furthermore, we prove the long-standing conjecture, that it is sufficient to restrict the order of primitive substitutions to the order of input formulae.