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 many classical theorems about Sturmian words in seconds, and are able to obtain new results about antisquares and antipalindromes in characteristic Sturmian words

翻译：我们展示了比普雷斯堡算术的Sturmian单词比普雷斯堡算术第一级理论是可分的。我们用一个一般补充器来确认Baranwal、Schaeffer和Shalit在Ostrowski计算系统中添加了Baranwal、Schaeffer和Shalit,我们证明,用一个单一的Sturmian单词来增加普雷斯堡计算法的第一阶次的扩展是统一的$\omega$自动的,然后推断出这类结构等级理论的可分性。我们通过执行这个称为Pecan的决定算法,在几秒钟内自动地对许多关于Sturmian单词的古典理论进行重新验证,并且能够从典型的Sturmian单词中获得关于反海藻和抗海平原的新结果。