BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:LCF-style Propositional Simplification With BDDs and SAT Solvers -
  Hasan Amjad (Middlesex University)
DTSTART:20080429T120000Z
DTEND:20080429T130000Z
UID:TALK11655@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:I'll talk about a new way of simplifying the propositional\nst
 ructure of terms in interactive theorem provers. The method uses Binary De
 cision Diagrams (BDDs) and SAT solvers\, but is fully LCF-style. I'll show
  how the method improves on standard rewrite-based simplifiers in both a l
 ogical and a practical sense.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR