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

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

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.