BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Compressing Translation from Propositional Resolution to Natural
  Deduction - Hasan Amjad (University of Cambridge)
DTSTART:20070529T120000Z
DTEND:20070529T130000Z
UID:TALK7413@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:I'll talk about caching identical parts of a SAT solver genera
 ted propositional resolution refutation proof in such a way that the resul
 ting smaller proof can be replayed in LCF-style natural deduction provers.
  The method can handle proofs with millions of inferences and proof is fas
 ter than with current methods. 
LOCATION:Computer Laboratory\, William Gates Building\, Room GS15
END:VEVENT
END:VCALENDAR