Automated Assistance for Proof Assistants

Larry Paulson

Colloquium in Honor of Gérard Huet, Paris 22-23 June 2007

Interactive proof assistants 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 theorems 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.