Abstract

Interactive theorem provers have been used to verify a wide variety of hardware and software systems. Unfortunately, they require too much effort from their users, especially beginners. We can reduce this effort by allowing our tools to call automatic theorem provers. A truly useful integration seems to require (1) “one-click” invocation, with no problem preparation; (2) background processing, so that users don’t have to wait for the results; (3) source-level proof reconstruction, so that expensive searches don’t have to be repeated. Background processing also allows the exploitation of multi- core architectures. All known facts are considered as candidate lemmas for assisting proofs. A simple relevance filtering algorithm selects a few hundred lemmas, to avoid overloading the automatic provers. Higher-order features are eliminated from problems by a translation that is compact, but potentially unsound; proof reconstruction ensures that only valid proofs are accepted.