Superposition for Full Higher-order Logic
Alexander Bentkamp, Jasmin Christian Blanchette, Sophie Tourret, Petar Vukmirović
Abstract
Abstract We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free $$\lambda $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>λ</mml:mi></mml:math> -superposition and superposition for first-order logic with interpreted Booleans. Stepping on these stones, we finally reach a sound and refutationally complete calculus for higher-order logic with polymorphism, extensionality, Hilbert choice, and Henkin semantics. In addition to the complexity of combining the calculus’s two predecessors, new challenges arise from the interplay between $$\lambda $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>λ</mml:mi></mml:math> -terms and Booleans. Our implementation in Zipperposition outperforms all other higher-order theorem provers and is on a par with an earlier, pragmatic prototype of Booleans in Zipperposition.