BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automation for Interactive Theorem Provers - Lawrence Paulson\, Co
 mputer Laboratory\, University of Cambridge
DTSTART:20071128T141500Z
DTEND:20071128T151500Z
UID:TALK8148@talks.cam.ac.uk
CONTACT:Timothy G. Griffin
DESCRIPTION:\n\n\nInteractive theorem provers have been used to verify a w
 ide variety\nof hardware and software systems. Unfortunately\, they requir
 e too\nmuch effort from their users\, especially beginners. We can reduce\
 nthis effort by allowing our tools to call automatic theorem provers.\nA t
 ruly useful integration seems to require (1) "one-click"\ninvocation\, wit
 h no problem preparation\; (2) background processing\,\nso that users don'
 t have to wait for the results\; (3) source-level\nproof reconstruction\, 
 so that expensive searches don't have to be\nrepeated. Background processi
 ng also allows the exploitation of multi-\ncore architectures. All known f
 acts are considered as candidate\nlemmas for assisting proofs. A simple re
 levance filtering algorithm\nselects a few hundred lemmas\, to avoid overl
 oading the automatic\nprovers. Higher-order features are eliminated from p
 roblems by a\ntranslation that is compact\, but potentially unsound\; proo
 f\nreconstruction ensures that only valid proofs are accepted.\n
LOCATION:Lecture Theatre 1\, Computer Laboratory
END:VEVENT
END:VCALENDAR