The Higher-Order Prover Leo-II.
The Higher-Order Prover Leo-II.
复制标题
DOI：
10.1007/s10817-015-9348-y
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Theiß F
中科院分区：
文献类型：
--
作者：
Benzmüller C;Sultana N;Paulson LC;Theiß F
Leo-II是经典高阶逻辑的自动定理证明器。该证明器开创了合作高阶一阶证明自动化，它影响了高阶逻辑的TPTP THF基础设施的发展，并已应用于广泛的问题。Leo-II还可以作为外部辅助工具调用校对助手，以节省用户的工作量。为此，Leo-II以标准化的语法返回证明信息至关重要，以便这些证明最终可以在证明助手中进行转换和验证。在这个方向上的最新进展报告的Isabelle/HOL系统。
Leo-II is an automated theorem prover for classical higher-order logic. The prover has pioneered cooperative higher-order–first-order proof automation, it has influenced the development of the TPTP THF infrastructure for higher-order logic, and it has been applied in a wide array of problems. Leo-II may also be called in proof assistants as an external aid tool to save user effort. For this it is crucial that Leo-II returns proof information in a standardised syntax, so that these proofs can eventually be transformed and verified within proof assistants. Recent progress in this direction is reported for the Isabelle/HOL system.
登录
查看更多内容
DOI：
10.4018/jswis.2012100105
发表时间：
2012-01-01
影响因子：
3.2
作者：
Alvez, Javier;Lucio, Paqui;Rigau, German
通讯作者：
Rigau, German
DOI：
10.1007/s10817-011-9233-2
发表时间：
2011-12-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Backes, Julian;Brown, Chad Edward
通讯作者：
Brown, Chad Edward
影响因子：
1
作者：
Benzmueller, Christoph;Paulson, Lawrence C.
通讯作者：
Paulson, Lawrence C.
DOI：
10.1007/s10472-011-9249-7
发表时间：
2011-06-01
影响因子：
1.2
作者：
Benzmueller, Christoph
通讯作者：
Benzmueller, Christoph
影响因子：
0.8
作者：
Benzmueller, Christoph;Paulson, Lawrence C.
通讯作者：
Paulson, Lawrence C.