Abstract: Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
Abstract: Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
复制标题
摘要：在证明助手中可靠地重建细粒度证明
DOI：
10.1007/978-3-030-79876-5_26
复制
发表时间：
2021
影响因子：
5.2
通讯作者：
Martin Desharnais
中科院分区：
文献类型：
--
作者：
Hans;M. Fleury;Martin Desharnais
我们提出了一个快速，可靠的重建证明所产生的SMT求解器veriT在伊莎贝尔。细粒度的证明格式使重建简单而有效。对于典型的证明步骤，如算术推理和skolemization，我们的重建可以避免昂贵的搜索。通过跳过与Isabelle无关的证明步骤，提高了证明检查的性能。我们的方法通过将失败率减半来提高大锤的成功率，并将检查时间减少13%。我们为每个规则的重建时间提供了详细的评估。运行时受经常出现的简单规则和常见复杂规则的影响。
We present a fast and reliable reconstruction of proofs generated by the SMT solver veriT in Isabelle. The fine-grained proof format makes the reconstruction simple and efficient. For typical proof steps, such as arithmetic reasoning and skolemization, our reconstruction can avoid expensive search. By skipping proof steps that are irrelevant for Isabelle, the performance of proof checking is improved. Our method increases the success rate of Sledgehammer by halving the failure rate and reduces the checking time by 13%. We provide a detailed evaluation of the reconstruction time for each rule. The runtime is influenced by both simple rules that appear very often and common complex rules.
MaSh：Sledgehammer 的机器学习
DOI：
10.1007/978-3-642-39634-2_6
发表时间：
2013
期刊：
影响因子：
--
作者：
Daniel Kühlwein;Jasmin Christian Blanchette;Cezary Kaliszyk;Josef Urban
通讯作者：
Josef Urban
来自机器生成的证明的半可理解的 Isar 证明
DOI：
10.1007/s10817-015-9335-3
发表时间：
2016
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jasmin Christian Blanchette;Sascha Böhme;Mathias Fleury;Steffen Juilf Smolka;Albert Steckermeier
通讯作者：
Albert Steckermeier
使用 SMT 求解器扩展 Sledgehammer
DOI：
10.1007/s10817-013-9278-5
发表时间：
2013
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jasmin Christian Blanchette;Sascha Böhme;Lawrence C. Paulson
通讯作者：
Lawrence C. Paulson