BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automated Reasoning and AI for Large Formal Mathematics - Josef Ur
 ban\, Czech Technical University in Prague
DTSTART:20160603T130000Z
DTEND:20160603T140000Z
UID:TALK65202@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:The first half of this talk will summarize several AI methods 
 for learning and reasoning developed over large formal math corpora. We wi
 ll show examples of AI systems implementing positive feedback loops betwee
 n learning and deduction\, and show the performance of the current methods
  over the Flyspeck\, Isabelle\, and Mizar libraries.  The second half will
  discuss AI methods that we have recently started to develop for automatin
 g the translation of informal mathematics to formal. These methods combine
  statistical parsing of informal mathematics with the large-theory theorem
  proving methods.
LOCATION:FW26
END:VEVENT
END:VCALENDAR