Скачать или смотреть Jeffrey Shallit: Experimental Combinatorics on Words Using the Walnut Prover

In this talk, I will show how to guess and prove theorems in combinatorics on words using the Walnut prover, written by Hamoon Mousavi. As an example, we recently proved the following result: the infinite word

r = 001001101101100100110110110010010011011001001001101100100100 ...

generated as the fixed point of the map a to abcab, b to cda, c to cdacd, d to abc, followed by the coding sending a, b to 0 and c, d to 1, is aperiodic and avoids the pattern x x x^R, where x^R denotes the reversal of x. This is the first nontrivial result on avoidance in words obtained through the use of a prover. This is joint work with Chen Fei Du, Hamoon Mousavi, Eric Rowland, and Luke Schaeffer.

Computationally Assisted Mathematical Discovery
and Experimental Mathematics: ACMES 2
12-15 May 2016, London, Ontario, Canada

Jeffrey Shallit, School of Computer Science, University of Waterloo
May 12, 2016

Visit the Rotman website for more information on applications, events, project descriptions and openings. http://www.rotman.uwo.ca

Follow The Rotman Institute on Twitter:   / rotmanphilo  

Like The Rotman Institute on Facebook:   / rotmanphilosophy  

Subscribe to our channel:    / rotmanphilosophy