# zbMATH — the first resource for mathematics

Superposition for lambda-free higher-order logic. (English) Zbl 07350767
Summary: We introduce refutationally complete superposition calculi for intentional and extensional clausal $$\lambda$$-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 $$\lambda$$-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.

##### MSC:
 03B70 Logic in computer science 68-XX Computer science
Full Text: