Superposition for full higher-order logic (Q2055874)

Superposition [\textit{L. Bachmair} and \textit{H. Ganzinger}, J. Log. Comput. 4, No. 3, 217--247 (1994; Zbl 0814.68117)] is a state-of-the-art inference system for automated theorem proving in classical first-order logic with equality. The problem of extending superposition to variants of classical higher-order logic has recently been gaining increasing attention. The authors essentially combine earlier work on superposition with Booleans [\textit{V. Nummelin} et al., Lect. Notes Comput. Sci. 12699, 378--395 (2021; Zbl 07437090)] and Boolean-free \(\lambda\)-superposition [\textit{A. Bentkamp} et al., J. Autom. Reasoning 65, No. 7, 893--940 (2021; Zbl 07433023)] to obtain a sound and refutationally complete superposition calculus for full rank-1 polymorphic classical higher-order logic which includes both Booleans and \(\lambda\)-expressions. A proof of refutational completeness is briefly sketched, with the details delegated to a technical report. 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)] and provide an experimental evaluation. The implementation outperforms all other higher-order theorem provers. For the entire collection see [Zbl 1475.68026].