Automation for Interactive Theorem Provers

Add to your list(s) Download to your calendar using vCal

• Lawrence Paulson, Computer Laboratory, University of Cambridge
• Wednesday 28 November 2007, 14:15-15:15
• Lecture Theatre 1, Computer Laboratory.

If you have a question about this talk, please contact Timothy G. Griffin.

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.

This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 1, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• Wednesday Seminars - Department of Computer Science and Technology
• bld31
• computer science
• se393's list

Note that ex-directory lists are not shown.