@inproceedings{5fa48785d37c4e25a9947a29143805d7,
title = "Making Higher-Order Superposition Work",
abstract = "{\textcopyright} 2021, The Author(s).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.",
author = "P. Vukmirovi{\'c} and A. Bentkamp and J. Blanchette and S. Cruanes and V. Nummelin and S. Tourret",
year = "2021",
doi = "10.1007/978-3-030-79876-5_24",
language = "English",
isbn = "9783030798758",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "415--432",
editor = "Andr{\'e} Platzer and Geoff Sutcliffe",
booktitle = "Automated Deduction – CADE 2021",
note = "28th International Conference on Automated Deduction, CADE 28 2021 ; Conference date: 12-07-2021 Through 15-07-2021",
}