| ||||
| ||||
![]() Title:Superposition for Lambda-Free Higher-Order Logic Conference:IJCAR-2018 Tags:applicative encoding, applicative first-order logic, higher-order logic, lambda-free higher-order logic, nonmonotonic term orders, refutational completeness, superposition and superposition calculus Abstract: We introduce refutationally complete superposition calculi for intentional and extensional lambda-free higher-order logic, a formalism that allows partial application and applied variables. The intentional variants perfectly coincide with standard superposition on first-order clauses. The calculi are parameterized by a well-founded term order that need not be compatible with arguments, 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 TPTP benchmarks. They appear promising as a stepping stone towards complete, efficient automatic theorem provers for full higher-order logic. Superposition for Lambda-Free Higher-Order Logic ![]() Superposition for Lambda-Free Higher-Order Logic | ||||
Copyright © 2002 – 2025 EasyChair |