与Lambda的叠加
Superposition with Lambdas
Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；Max-Planck-Institut für Informatik（马克斯·普朗克信息学研究所）
摘要：
我们设计了一个叠加演算的延伸多态高阶逻辑，包括匿名函数，但不包括布尔的子句片段。推理规则作用于$λ$-项的$βη$-等价类，并依赖于高阶统一来实现反驳完备性。我们在Zipperposition证明器中实现了微积分，并在TPTP和Isabelle基准测试中进行了评估。结果表明，叠加是一个合适的基础高阶推理。
英文摘要：
We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $βη$-equivalence classes of $λ$-terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle benchmarks. The results suggest that superposition is a suitable basis for higher-order reasoning.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
