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.
Cite
CITATION STYLE
Bentkamp, A., Blanchette, J. C., Cruanes, S., & Waldmann, U. (2018). Superposition for Lambda-Free Higher-Order Logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10900 LNAI, pp. 28–46). Springer Verlag. https://doi.org/10.1007/978-3-319-94205-6_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
