Superposition for Lambda-Free Higher-Order Logic

Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes +1

We introduce refutationally complete superposition calculi for intentional and extensional clausal $\lambda$-free higher-order logic, two formalisms that allow partial application and ap…