We show that the first-order theory of Sturmian words over Presburger arithmetic is decidable. Using a general adder recognizing addition in Ostrowski numeration systems by Baranwal, Schaeffer and Shallit, we prove that the first-order expansions of Presburger arithmetic by a single Sturmian word are uniformly $\omega$-automatic, and then deduce the decidability of the theory of the class of such structures. Using an implementation of this decision algorithm called Pecan, we automatically reprove classical theorems about Sturmian words in seconds, and are able to obtain new results about antisquares and antipalindromes in characteristic Sturmian words.

翻译：我们证明，关于Presburger算术的Sturmian词的一阶理论是可判定的。利用Baranwal、Schaeffer和Shallit在Ostrowski计数系统中识别加法的一般加法器，我们证明由单个Sturmian词扩展的Presburger算术的一阶展开是均匀$\omega$-自动的，进而推导出该类结构理论的可行性。通过使用名为Pecan的该判定算法的实现，我们在数秒内自动重新证明了关于Sturmian词的经典定理，并能够获得关于特征Sturmian词中反平方与反回文的新结果。