Sledgehammer: Judgement Day
Sledgehammer: Judgement Day
复制标题
大锤：审判日
DOI：
10.1007/978-3-642-14203-1_9
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
T. Nipkow
中科院分区：
文献类型：
--
作者：
S. Böhme;T. Nipkow
Sledgehammer 是交互式定理证明器 Isabelle 的一个组件，通过调用一阶逻辑 E、SPASS 和 Vampire 的自动证明器来查找高阶逻辑的证明。这篇论文是迄今为止对这种联系最大、最详细的实证评估。我们的测试数据由 7 种不同的 Isabelle 理论中产生的 1240 个证明目标组成，从而代表了典型的 Isabelle 证明义务。我们衡量 Sledgehammer 的有效性以及许多其他参数，例如运行时间和证明的复杂性。提出并分析了一种最小化证明目标所需事实数量的工具。
Sledgehammer, a component of the interactive theorem prover Isabelle, finds proofs in higher-order logic by calling the automated provers for first-order logic E, SPASS and Vampire. This paper is the largest and most detailed empirical evaluation of such a link to date. Our test data consists of 1240 proof goals arising in 7 diverse Isabelle theories, thus representing typical Isabelle proof obligations. We measure the effectiveness of Sledgehammer and many other parameters such as run time and complexity of proofs. A facility for minimizing the number of facts needed to prove a goal is presented and analyzed.