Hammering towards QED
Hammering towards QED
复制标题
DOI：
10.6092/issn.1972-5787/4593
复制
发表时间：
2016-01-01
影响因子：
--
通讯作者：
Urban, Josef
中科院分区：
文献类型：
--
作者：
Blanchette, Jasmin C.;Kaliszyk, Cezary;Urban, Josef
本文调查了新兴方法，以自动推理与正式证明助手开发的大型图书馆。我们称这些方法锤。它们为作者提供了正式证明的作者一个强大的“一冲程”工具，可以在不需要仔细详细的手动编程证明搜索的情况下放电困难的引理。这种方法的主要成分是有效的自动定理抛光剂，可以应对数百个公理，将证明助手的逻辑译成自动掠夺，启发式和学习方法的合适翻译，从大型库中选择相关事实，以及重建自动在证明助手中找到的证据。我们概述了这些方法的历史，解释主要问题和技术，并在几个大型基准上显示其实力。我们还讨论了该技术与QED宣言的关系，并考虑了其对QED式努力的影响。
This paper surveys the emerging methods to automate reasoning over large libraries developed with formal proof assistants. We call these methods hammers. They give the authors of formal proofs a strong "one-stroke" tool for discharging difficult lemmas without the need for careful and detailed manual programming of proof search.The main ingredients underlying this approach are efficient automatic theorem provers that can cope with hundreds of axioms, suitable translations of the proof assistant's logic to the logic of the automatic provers, heuristic and learning methods that select relevant facts from large libraries, and methods that reconstruct the automatically found proofs inside the proof assistants.We outline the history of these methods, explain the main issues and techniques, and show their strength on several large benchmarks. We also discuss the relation of this technology to the QED Manifesto and consider its implications for QED-like efforts.