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

https://hal.inria.fr/hal-03364024
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

File

conf.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

40

Files downloads

46