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
DTSTART:20160603T130000Z
DTEND:20160603T140000Z
UID:TALK66433@talks.cam.ac.uk
CONTACT:Louise Segar
DESCRIPTION:The first half of this talk will summarize several AI methods 
 for\nlearning and reasoning developed over large formal math corpora. We\n
 will show examples of AI systems implementing positive feedback loops\nbet
 ween learning and deduction\, and show the performance of the\ncurrent met
 hods over the Flyspeck\, Isabelle\, and Mizar libraries. The\nsecond half 
 will discuss AI methods that we have recently started to\ndevelop for auto
 mating the translation of informal mathematics to\nformal. These methods c
 ombine statistical parsing of informal\nmathematics with the large-theory 
 theorem proving methods.\n
LOCATION:William Gates Building - FW26
END:VEVENT
END:VCALENDAR