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

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

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.