University of Cambridge > Talks.cam > Computer Laboratory Wednesday Seminars > Automation for Interactive Theorem Provers

Automation for Interactive Theorem Provers

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

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 Computer Laboratory Wednesday Seminars series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity