Sturmian字的可判定性
Decidability for Sturmian words
AI总结：
该研究证明Presburger算术上Sturmian字的一阶理论可判定，借助通用加法器论证其一致ω-自动性，并用Pecan算法实现复现经典定理、得到特征Sturmian字中反平方与反回文的新结果。
摘要：
我们证明了Presburger算术上Sturmian字的一阶理论是可判定的。借助Baranwal、Schaeffer和Shallit提出的可识别Ostrowski记数系统中加法的通用加法器，我们证明了由单个Sturmian字扩展的Presburger算术一阶结构是一致ω-自动的，进而推导出这类结构类理论的可判定性。利用名为Pecan的该判定算法实现，我们在数秒内自动重新证明了关于Sturmian字的经典定理，还得到了特征Sturmian字中反平方和反回文的新结果。
英文摘要：
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 $ω$-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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
