Superposition for Lambda-Free Higher-Order Logic

Alexander Bentkamp (1) , Jasmin Blanchette (2, 1) , Simon Cruanes (3) , Uwe Waldmann (4)

1 VU - Vrije Universiteit Amsterdam [Amsterdam]
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
3 Aesthetic Integration
4 MPI - Max Planck Institute of Experimental Medicine [Göttingen]

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.

Mots clés: superposition calculus; Boolean-free lambda-free higher-order logic; refutational completeness. Extended version of Bentkamp et al.; "Superposition for lambda-free higher-order logic" [BBCW18]

Domaines: Logique en informatique [cs.LO]

Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann. Superposition for Lambda-Free Higher-Order Logic. Logical Methods in Computer Science, 2021, 17 (2), ⟨10.23638/LMCS-17(2:1)2021⟩. ⟨hal-03485227⟩