Is Büchi's theorem useful for you? (for an audience of logicians)

Almost a century ago, Presburger showed that the first order theory of the natural numbers with addition is decidable. Following the work of Büchi in 1960, this result still holds when adding a function $V_k$ to the structure, where $V_k(n)$ is the largest power of $k\ge 2$ diving $n$. In particular, this leads to a logical characterization of the $k$-automatic sequences. During the last few years, many applications of this result have been considered in combinatorics on words, mostly by J. Shallit and his coauthors. In this talk, we will present this theorem of Büchi where decidability relies on finite automata. Then we will review some results about automatic sequences or morphic words that can be proved automatically (i.e., the proof is carried on by an algorithm). Finally, we will sketch the limitation of this technique. With a single line formula, one can prove automatically that the Thue-Morse word has no overlap but, hopefully, not all the combinatorial properties of morphic words can be derived in this way. We will not assume any background in combinatorics on words from the audience.