A Combinator-Based Superposition Calculus for Higher-Order Logic
A Combinator-Based Superposition Calculus for Higher-Order Logic
复制标题
DOI：
10.1007/978-3-030-51074-9_16
复制
发表时间：
2020-05-30
期刊：
影响因子：
--
通讯作者：
Reger G
中科院分区：
文献类型：
--
作者：
Bhayat A;Reger G
我们提出了一个版本的高阶逻辑的组合演算的基础上的反驳完全叠加演算。我们还介绍了一种新的方法来处理外延。该演算在Vampire定理证明器中实现，我们针对其他领先的高阶证明器测试了其性能。结果表明，该方法具有竞争力。
We present a refutationally complete superposition calculus for a version of higher-order logic based on the combinatory calculus. We also introduce a novel method of dealing with extensionality. The calculus was implemented in the Vampire theorem prover and we test its performance against other leading higher-order provers. The results suggest that the method is competitive.
登录
查看更多内容
DOI：
10.1007/s10817-015-9348-y
发表时间：
2015
期刊：
Journal of automated reasoning
影响因子：
--
作者：
Benzmüller C;Sultana N;Paulson LC;Theiß F
通讯作者：
Theiß F
DOI：
10.1007/s10817-017-9407-7
发表时间：
2017-12-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Sutcliffe, Geoff
通讯作者：
Sutcliffe, Geoff
DOI：
10.1007/s10817-018-9458-4
发表时间：
2018
期刊：
Journal of automated reasoning
影响因子：
--
作者：
Czajka Ł;Kaliszyk C
通讯作者：
Kaliszyk C
DOI：
10.1007/s10817-007-9085-y
发表时间：
2008-01-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Meng, Jia;Paulson, Lawrence C.
通讯作者：
Paulson, Lawrence C.