A calculus and a system architecture for extensional higher-order resolution

Abstract: "The first part of this paper introduces an extension for a variant of Huet's higher-order resolution calculus [Hue72, Hue73] based upon classical type theory (Church's typed [lambda]-calculus [Chu40]) in order to obtain a calculus which is complete with respect to Henkin models [Hen50]. The new rules connect higher-order pre-unification with the general refutation process in an appropriate way to establish full extensionality for the whole system. The general idea of the calculus is discussed on different examples. The second part introduces the Leo system which implements the discussed extensional higher-order resolution calculus. This part mainly focus [sic] on the embedding of the new extensionality rules into the refutation process and the treatment of higher-order unification.