Superposition with Lambdas

To increase automation in proof assistants and other verification tools based on higher-order formalisms, we propose to generalize superposition to an extensional, polymorphic, clausal version of higher-order logic (also called simple type theory). Our ambition is to achieve a graceful extension, which coincides with standard superposition on first-order problems and smoothly scales up to arbitrary higher-order problems. Bentkamp, Blanchette, Cruanes, and Waldmann [12] designed a family of superpositionlike calculi for a λ-free clausal fragment of higher-order logic, with currying and applied variables. We adapt their extensional nonpurifying calculus to support λ-terms (Sect.