Model Theory behind Automated Theorem Proving (series unlisted)

Abstract: In 2011, a Japanese research institute started a project called “Todai Robot Project – Can a Robot Pass the University of Tokyo Entrance Exam?” To solve math problems, their artificial intelligence heavily relied on an algorithm for quantifier elimination 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 talk, I’m going to introduce very basic model theory to explain what Tarski proved and how to use it. Of course, I’ll talk about the result of Todai Robot Project too.

Mathematics

Audience: general audience

Pizza Seminar