BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Validating QBF Invalidity in HOL4 - Tjark Weber (University of Cam
 bridge)
DTSTART:20100601T120000Z
DTEND:20100601T130000Z
UID:TALK24362@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:The Quantified Boolean Formulae (QBF) solver Squolem can gener
 ate certificates of invalidity\, based on Q-resolution. I present independ
 ent checking of these certificates in the HOL4 theorem prover. This enable
 s\nHOL4 users to benefit from Squolem's automation for QBF problems\, and 
 provides high correctness assurances for Squolem's results. Detailed perfo
 rmance data shows that LCF-style certificate checking is feasible even for
  large QBF instances. The work prompted improvements to HOL4's\ninference 
 kernel.\n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR