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.