Adventures in Automata with a Theorem-Prover

Overview

About the Talk:

Wouldn’t it be nice if one could simply state a theorem that you don’t know how to prove, and then have a computer do all the work? Of course, this is impossible in general, but decision procedures do exist for some small domains. Combinatorics on words is one such domain. In this talk I will describe how automata play a crucial role in designing a theorem-prover called “Walnut”, and the wide variety of results one can prove with it. Dozens of results published in the literature can be reproved in seconds with almost no effort, and two incorrect results in the literature were corrected. In addition, Walnut can be used to prove many new results.

Biography of Speaker:
Jeffrey Shallit is a professor in the School of Computer Science at the University of Waterloo, where he has taught since 1990. He is a foreign member of the Finnish Academy of Science and Letters. He received an AB from Princeton University in 1979 and a Ph.D. from the University of California, Berkeley, in 1983. His research areas include formal languages, finite automata, combinatorics on words, algorithmic number theory, algebra, and history of mathematics, and he has published approximately 300 articles on these topics since 1975. He is also the author or co-author of four books.