# Superposition for Full Higher-order Logic

2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
5 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free $\lambda$-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’s two predecessors, new challenges arise from the interplay between $\lambda$-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.
Document type :
Conference papers

https://hal.inria.fr/hal-03364032
Contributor : Jasmin Blanchette Connect in order to contact the contributor
Submitted on : Monday, October 4, 2021 - 1:19:37 PM
Last modification on : Monday, February 14, 2022 - 8:14:17 PM
Long-term archiving on: : Wednesday, January 5, 2022 - 6:31:27 PM

### File

conf.pdf
Files produced by the author(s)

### Citation

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović. Superposition for Full Higher-order Logic. CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA / online, United States. pp.396-412, ⟨10.1007/978-3-030-79876-5_23⟩. ⟨hal-03364032⟩

Record views