# Events & News

# CS Colloquium

Category | Lecture |

Date | Thursday, January 28, 2016 |

Time | 11:00 am |

Concludes | 12:15 pm |

Location | Gould-Simpson 906 |

Details | Please join us for coffee and light refreshments at 10:45am, Gould-Simpson, 9th Floor Atrium. Faculty Host: Along Efrat |

Speaker | Jeffrey Shallit |

Title | Ph.D. |

Affiliation | Computer 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.

## Biography

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).