Superposition for Lambda-Free Higher-Order Logic

Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann

Research output: Contribution to JournalArticleAcademicpeer-review


© A. Bentkamp, J. Blanchette, S. Cruanes, and U. Waldmann.We introduce refutationally complete superposition calculi for intentional and extensional clausal λ-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 Isabelle/HOL and TPTP benchmarks. They appear promising as a stepping stone towards complete, highly efficient automatic theorem provers for full higher-order logic.
Original languageEnglish
Article number1
Pages (from-to)1:1–1:38
Number of pages38
JournalLogical Methods in Computer Science
Issue number2
Publication statusPublished - 12 Apr 2021


Dive into the research topics of 'Superposition for Lambda-Free Higher-Order Logic'. Together they form a unique fingerprint.

Cite this