Hardening the Hammer: More Integration of Automatic and Interactive Theorem Provers

强化锤子：自动和交互式定理证明器的更多集成

• 批准号: 226154341
• 负责人: Professor Dr. Tobias Nipkow, Ph.D.
• 金额: --
• 依托单位: Lehrstuhl für Informatik XXI: Logik und Verifikation
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2012
• 资助国家: 德国
• 起止时间: 2011-12-31 至 2015-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/226154341?language=en
• 关键词: Hardening; Hammer; More; Integration; Automatic

Interactive theorem provers (ITPs) are increasingly used for verifying the correctness of complex and safety-critical algorithms and systems. ITPs support expressive logics but are very laborious to use. In contrast, automatic theorem provers (ATPs) focus on simpler logics that can be automated better. This proposal promises to narrow the gap between ITPs and ATPs further to achieve a higher level of automation for ITPs, thus permitting them to perform more complex proofs in less time.The platform for our work is the widely used ITP Isabelle/HOL. Sledgehammer is a subsystem of Isabelle/HOL. It provides an integration with the most powerful ATPs ¿on the market¿ to assist with interactive proof construction. Sledgehammer has been available for nearly five years, and in that time it has become an essential part of the Isabelle user's workflow. It is undoubtedly the only interface between an ITP and ATPs to achieve such popularity with users. It has transformed the way beginners perceive Isabelle.This project will extend the ITP/ATP integration in a number of fundamental respects. Currently Sledgehammer proofs are black boxes one cannot examine; now we want to extract human-readable proofs from the machine-level resolution proofs that ATPs produce. Currently Sledgehammer is restricted to one logic, HOL; now we want to extend it to set theory, the de facto foundation of mathematics and also the foundation of Lamport¿s TLA+, a logic and system for software specification and verification. Currently Sledgehammer performs poorly on sets and other higher-order constructs; now we want to design and evaluate new encodings for higher-order constructs in first-order logic (as supported by the ATPs). Currently Sledgehammer targets untyped first-order logic; now we want to benefit from recent advances in ATP technology in the areas of type systems and built-in theories.Important aspects of our proposal are the large user base for Isabelle that will benefit from the research, the large amount of data in the form of proofs that our empirical evaluations are based on, and our close interaction with the ATP community to guarantee an optimal fit of the logics and type systems of ATPs and ITPs.

交互式定理证明器（ITP）越来越多地用于验证复杂和安全关键算法和系统的正确性。ITP支持表达逻辑，但使用起来非常费力。相比之下，自动定理证明器（ATP）专注于可以更好地自动化的简单逻辑。该建议有望缩小ITP和ATP之间的差距，进一步实现ITP的自动化水平更高，从而使他们能够在更短的时间内完成更复杂的证明。我们工作的平台是广泛使用的ITP Isabelle/HOL。Sledgehammer是Isabelle/HOL的一个子系统。它提供了与市场上最强大的ATP的集成，以协助交互式证明构建。Sledgehammer已经可用了将近五年，在这段时间里，它已经成为Isabelle用户工作流程的重要组成部分。毫无疑问，它是ITP和ATP之间唯一的接口，可以在用户中实现这种普及。它改变了初学者对Isabelle的看法。这个项目将在一些基本方面扩展ITP/ATP集成。目前，大锤证明是一个无法检查的黑盒子;现在我们想从ATP产生的机器级分辨率证明中提取人类可读的证明。目前大锤仅限于一个逻辑，HOL;现在我们希望将其扩展到集合论，数学的事实基础，也是Lamport的TLA+的基础，这是一个用于软件规范和验证的逻辑和系统。目前，Sledgehammer在集合和其他高阶结构上表现不佳;现在我们想设计和评估一阶逻辑中高阶结构的新编码（如ATP所支持的）。目前大锤的目标是无类型的一阶逻辑;现在，我们希望从ATP技术在类型系统和内置理论领域的最新进展中受益。我们建议的重要方面是Isabelle的大量用户群将从研究中受益，我们的经验评估所基于的大量数据以证据的形式存在，以及我们与ATP社区的密切互动，以确保ATP和ITP的逻辑和类型系统的最佳匹配。

项目成果

A Learning-Based Fact Selector for Isabelle/HOL

• DOI: 10.1007/s10817-016-9362-8
• 发表时间: 2016-10-01
• 期刊: JOURNAL OF AUTOMATED REASONING
• 作者: Blanchette, Jasmin Christian;Greenaway, David;Urban, Josef
• 通讯作者: Urban, Josef

Extending Sledgehammer with SMT Solvers

使用 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

Semi-intelligible Isar Proofs from Machine-Generated Proofs

来自机器生成的证明的半可理解的 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

Hammering towards QED

• DOI: 10.6092/issn.1972-5787/4593
• 发表时间: 2016-01-01
• 期刊: JOURNAL OF FORMALIZED REASONING
• 作者: Blanchette, Jasmin C.;Kaliszyk, Cezary;Urban, Josef
• 通讯作者: Urban, Josef