Skip to Main content Skip to Navigation
New interface
Conference papers

Superposition for Lambda-Free Higher-Order Logic

Abstract : We introduce refutationally complete superposition calculi for intentional and extensional λ-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the λ-free higher-order lexicographic path and Knuth-Bendix orders. We implemented the calculi in the Zipperposition prover and evaluated them on TPTP benchmarks. They appear promising as a stepping stone towards complete, efficient automatic theorem provers for full higher-order logic.
Document type :
Conference papers
Complete list of metadata

Cited literature [47 references]  Display  Hide  Download
Contributor : Jasmin Blanchette Connect in order to contact the contributor
Submitted on : Thursday, October 25, 2018 - 10:45:50 AM
Last modification on : Wednesday, March 9, 2022 - 3:10:44 AM
Long-term archiving on: : Saturday, January 26, 2019 - 1:37:28 PM


Files produced by the author(s)


  • HAL Id : hal-01904595, version 1



Alexander Bentkamp, Simon Cruanes, Jasmin Christian Blanchette, Uwe Waldmann. Superposition for Lambda-Free Higher-Order Logic. IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. ⟨hal-01904595⟩



Record views


Files downloads