Skip to Main content Skip to Navigation
Conference papers

Making Higher-Order Superposition Work

Abstract : Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about formulas, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.
Document type :
Conference papers
Complete list of metadata
Contributor : Jasmin Blanchette Connect in order to contact the contributor
Submitted on : Monday, October 4, 2021 - 1:09:07 PM
Last modification on : Monday, February 14, 2022 - 8:12:19 PM
Long-term archiving on: : Wednesday, January 5, 2022 - 6:30:46 PM


Files produced by the author(s)




Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, et al.. Making Higher-Order Superposition Work. CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA / online, United States. pp.415-432, ⟨10.1007/978-3-030-79876-5_24⟩. ⟨hal-03364024⟩



Record views


Files downloads