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

点击翻译按钮获取中文摘要

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.