一句话：证明在 Presburger 算术上加入单个 Sturmian 词的一阶理论可判定，并实现 Pecan 自动证明相关定理。
本文研究 Sturmian 词的一阶理论可判定性。作者利用 Baranwal、Schaeffer 与 Shallit 给出的、可在 Ostrowski 记数系统中识别加法的通用加法器，证明 Presburger 算术由单个 Sturmian 词作一阶扩张后具有一致 ω-自动结构，由此推出该类结构理论的可判定性。基于该判定算法实现工具 Pecan，可在数秒内自动重证 Sturmian 词的经典定理，并得到关于特征 Sturmian 词中 antisquares 与 antipalindromes 的新结果。
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.
@article{paperbot2738,
title = {Decidability for Sturmian words},
author = {Philipp Hieronymi and Dun Ma and Reed Oei and Luke Schaeffer and Christian Schulz and Jeffrey Shallit},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 3},
year = {2024},
doi = {10.46298/lmcs-20(3:12)2024}
}