@inproceedings{aecf15db2eab482f874de78d276b5caa,
title = "Superposition for Full Higher-Order Logic",
abstract = "We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free λ -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{\textquoteright}s two predecessors, new challenges arise from the interplay between λ -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.",
author = "A. Bentkamp and J. Blanchette and S. Tourret and P. Vukmirovi{\'c}",
year = "2021",
doi = "10.1007/978-3-030-79876-5_23",
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 = "396--412",
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",
}