The University of Arizona

Events & News

CS Colloquium

DateThursday, January 28, 2016
Time11:00 am
Concludes12:15 pm
LocationGould-Simpson 906
DetailsPlease join us for coffee and light refreshments at 10:45am, Gould-Simpson, 9th Floor Atrium.

Faculty Host: Along Efrat
SpeakerJeffrey Shallit
AffiliationComputer Science Department, University of Waterloo

Automatically Proving Theorems in Combinatorics on Words Using a Computer

Combinatorics on words is the study of (finite or infinite)
strings of symbols. A famous example of an infinite string is the
Thue-Morse word t = 0110100110010110..., in which the n'th term is
0 or 1 according to whether the sum of the digits of n, when expressed
in base 2, is even or odd. More than a hundred years ago, the Norwegian mathematician Axel Thue famously proved that that t contains no overlaps, that is, no blocks of the form AAa, where a is the first
letter of the block A. In this talk, I will discuss how results like
Thue's can be proved purely mechanically, using a decision procedure.
Our implementation of this decision procedure has succeeded in proving
many results from the literature, and also many new results.


Jeffrey Shallit is Professor of Computer Science at the University of
Waterloo, Canada. He works in formal languages, combinatorics on words, number theory, automata theory, logic, and algebra. He is an ACM Distinguished Scientist.

He has published four books: Algorithmic Number Theory (with Eric Bach); Automatic Sequences (with Jean-Paul Allouche); A Second Course in Automata Theory and Formal Languages; and Neverending Fractions (with Jon Borwein, Alf van der Poorten, and Wadim Zudilin).