Logical Framework and Decidability Issues
Michel Rigo · 2014
This chapter explains that every k-automatic word can be defined using a first-order formula in an appropriate logical structure that is an extension of the Presburger arithmetic. It presents the Presburger arithmetic, and discusses the decidability of this theory using the classical technique of the elimination of quantifiers. Büchi's theorem is also presented. This is followed by a discussion on some corollaries of üchi's theorem and possible applications to combinatorics on words such as proving or disproving the occurrence of repetitions or overlaps. The chapter explains how some properties about 2-automatic words, like the Thue–Morse word, can be explored. It concludes with a discussion on Abelian unbordered factors, periodicity, and applications to Pisot numeration systems.