Tags:automatic theorem proving, higher-order logic and superposition

Abstract:

Lambda-superposition is a proof calculus for higher-order logic (simple type theory) developed in collaboration with Alexander Bentkamp, Simon Cruanes, Visa Nummelin, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. 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 the lambda-superposition refutationally complete. On the practical side, we implemented it in the Zipperposition prover and, together with Stephan Schulz, in the E prover. 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.