BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Computer Laboratory Automated Reasoning Group Lunc
 hes
SUMMARY:SMT Solvers: New Oracles for the HOL Theorem Prove
 r - Tjark Weber (University of Cambridge)
DTSTART;TZID=Europe/London:20091117T130000
DTEND;TZID=Europe/London:20091117T140000
UID:TALK19690AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/19690
DESCRIPTION:I will describe an integration of Satisfiability M
 odulo Theories (SMT) solvers with the HOL4 theorem
  prover.  Proof obligations are passed from the in
 teractive HOL4 prover to the SMT solver\, which ca
 n often prove them automatically.  This makes stat
 e-of-the-art SMT solving techniques available to u
 sers of the HOL4 system\, thereby\nincreasing the 
 degree of automation for a substantial fragment of
  its logic.  A translation to Yices's native input
  format is compared with a translation to SMT-LIB 
 format.\n
LOCATION:Computer Laboratory\, William Gates Building\, Roo
 m SS03
CONTACT:Thomas Tuerk
END:VEVENT
END:VCALENDAR