Superposition with lambdas (Q5919500)

Superposition [\textit{L. Bachmair} and \textit{H. Ganzinger}, J. Log. Comput. 4, No. 3, 217--247 (1994; Zbl 0814.68117)] is the state-of-the-art inference system for automated theorem proving in classical first-order logic with equality. The authors, basing on earlier work [\textit{A. Bentkamp} et al., Log. Methods Comput. Sci. 17, No. 2, Paper No. 1, 38 p. (2021; Zbl 07350767)], extend superposition to a clausal fragment of classical extensional rank-1 polymorphic higher-order logic which includes \(\lambda\)-expressions but excludes Booleans. A proof of refutational completeness for the core calculus is sketched, with an accompanying technical report containing the details. Some extensions of the core calculus to make it more practical are outlined. Finally, the authors describe the implementation of their superposition calculus in the Zipperposition prover [\textit{S. Cruanes}, Lect. Notes Comput. Sci. 10483, 172--188 (2017; Zbl 1496.68365)]. An experimental evaluation of the implementation is provided. For the entire collection see [Zbl 1428.68018].