BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:SMT Solvers: New Oracles for the HOL Theorem Prover - Tjark Weber 
 (University of Cambridge)
DTSTART:20091117T130000Z
DTEND:20091117T140000Z
UID:TALK19690@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:I will describe an integration of Satisfiability Modulo Theori
 es (SMT) solvers with the HOL4 theorem prover.  Proof obligations are pass
 ed from the interactive HOL4 prover to the SMT solver\, which can often pr
 ove them automatically.  This makes state-of-the-art SMT solving technique
 s available to users of the HOL4 system\, thereby\nincreasing the degree o
 f automation for a substantial fragment of its logic.  A translation to Yi
 ces's native input format is compared with a translation to SMT-LIB format
 .\n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR