一句话：为无 λ 高阶逻辑提出反驳完备的叠加演算，支持部分应用和应用变量，并在 Zipperposition 中实现评估。
论文研究如何将一阶叠加演算推广到无 λ 的高阶逻辑，以支持部分应用与应用变量，并同时处理内涵和外延两种语义。作者提出两个反驳完备的叠加演算，二者可由不一定完全单调的项序参数化，从而可采用无 λ 高阶字典序路径序与 Knuth-Bendix 序。演算已在 Zipperposition 证明器中实现，并在 Isabelle/HOL 与 TPTP 基准上评估。实验表明这些演算有望成为迈向完整且高效的全高阶逻辑自动定理证明器的垫脚石。
We introduce refutationally complete superposition calculi for intentional and extensional clausal $\lambda$-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 $\lambda$-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.Comment: arXiv admin note: text overlap with arXiv:2102.00453
@article{paperbot1327,
title = {Superposition for Lambda-Free Higher-Order Logic},
author = {Alexander Bentkamp and Jasmin Blanchette and Simon Cruanes and Uwe Waldmann},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 2},
year = {2021},
doi = {10.23638/lmcs-17(2:1)2021}
}