COPLAS Talk: Lambda-Superposition: From Theory to Trophy
Speaker
Jasmin Blanchette, LMU München
Title
Lambda-Superposition: From Theory to Trophy
Joint work with Alexander Bentkamp, Simon Cruanes, Visa Nummelin, Stephan Schulz, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann
Abstract
Lambda-superposition is a new proof calculus for higher-order logic. To a large extent, the calculus is a graceful generalization of standard superposition, which is a highly successful calculi for first-order logic. On the theory side, we proved lambda-superposition refutationally complete. On the practical side, we implemented it in the E and Zipperposition provers. Zipperposition finished first in the higher-order theorem division of the CADE ATP System Competition in 2020, 2021, and 2022, suggesting that superposition is a valuable approach also in a higher-order setting.