COPLAS Talk: Lambda-Superposition: From Theory to Trophy



Jasmin Blanchette, LMU München


Lambda-Superposition: From Theory to Trophy

Joint work with Alexander Bentkamp, Simon Cruanes, Visa Nummelin, Stephan Schulz, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann


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.


Read about Jasmin here.

Zoom link

All are welcome. No registration is required.