Superposition for Lambda-Free Higher-Order Logic

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.
Document type :
Conference papers
Liste complète des métadonnées

https://hal.inria.fr/hal-01904595
Contributor : Jasmin Christian Blanchette <>
Submitted on : Thursday, October 25, 2018 - 10:45:50 AM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Document(s) archivé(s) le : Saturday, January 26, 2019 - 1:37:28 PM

File

lfhosup_paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01904595, version 1

Collections

Citation

Alexander Bentkamp, Simon Cruanes, Jasmin Christian Blanchette, Uwe Waldmann. Superposition for Lambda-Free Higher-Order Logic. IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. ⟨hal-01904595⟩

Share

Metrics

Record views

61

Files downloads

14