BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Takehiko Gappo
DTSTART:20210205T184000Z
DTEND:20210205T194000Z
DTSTAMP:20260423T004729Z
UID:Pizza/14
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/Pizza/14/">M
 odel Theory behind Automated Theorem Proving</a>\nby Takehiko Gappo as par
 t of Pizza Seminar\n\n\nAbstract\nIn 2011\, a Japanese research institute 
 started a project called “Todai Robot Project – Can a Robot Pass the U
 niversity of Tokyo Entrance Exam?” To solve math problems\, their artifi
 cial intelligence heavily relied on an algorithm for quantifier eliminatio
 n for real closed fields\, which was first discovered by Tarski in 1930’
 s and regarded as one of the earliest theorems in model theory. In this ta
 lk\, I’m going to introduce very basic model theory to explain what Tars
 ki proved and how to use it. Of course\, I’ll talk about the result of T
 odai Robot Project too.\n
LOCATION:https://researchseminars.org/talk/Pizza/14/
END:VEVENT
END:VCALENDAR