论文标题
无LAMBDA的高阶逻辑的叠加
Superposition for Lambda-Free Higher-Order Logic
论文作者
论文摘要
我们介绍了针对故意和延长的clausal $λ$的反驳叠加表结石，无需无限的高阶逻辑，两种形式主义允许部分应用和应用变量。骨子通过不需要完全单调的定期顺序进行参数化，从而可以采用$λ$的高级词典路径和Knuth-Bendix订单。我们在拉链置换者中实现了骨化器，并在isabelle/hol和TPTP基准测试中对其进行了评估。它们似乎是垫脚石，朝着完整的，高效的自动定理抛弃，以实现完整的高阶逻辑。
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.
