BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Finite Model Generation\, Proof-Producing SAT Solvers\, and SMT - 
 Tjark Weber (University of Cambridge)
DTSTART:20090203T130000Z
DTEND:20090203T140000Z
UID:TALK16354@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:This talk consists of three parts. First\, I will present a fi
 nite model generator for higher-order logic. The input formula is translat
 ed to propositional logic\, so that a standard SAT solver can be employed 
 for the actual model search.  The model generator supports many of the\nde
 finitional mechanisms available in the Isabelle/HOL theorem prover\, and h
 as been applied to various case studies.\n\nSecond\, I will present an int
 egration of proof-producing SAT solvers with higher-order logic theorem pr
 overs.  An adequate representation of the SAT problem allows to verify uns
 atisfiability proofs with millions of resolutions steps.\n\nLast\, I will 
 give a brief introduction to Satisfiability Modulo Theories (SMT)\, the de
 cision problem for first-order formulae with respect to combinations of ba
 ckground theories.\n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR