DOI: 10.1145/3636362.3636367 ISSN: 2372-3491
Complete and Efficient Higher-Order Reasoning via Lambda-Superposition
Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Uwe Waldmann- General Earth and Planetary Sciences
- General Environmental Science
Superposition is a highly successful proof calculus for reasoning about first-order logic with equality. We present λ-superposition, which extends superposition to higher-order logic. Its design goals include soundness, completeness, efficiency, and gracefulness with respect to standard first-order superposition. The calculus is implemented in two automatic theorem provers: E and Zipper position. These provers regularly win trophies at the CADE ATP System Competition, confirming the calculus's applicability. This paper is a summary of research that took place between 2017 and 2022.