TY - GEN
T1 - Decidability for Sturmian Words
AU - Hieronymi, Philipp
AU - Ma, Dun
AU - Oei, Reed
AU - Schaeffer, Luke
AU - Schulz, Christian
AU - Shallit, Jeffrey
N1 - Funding Information:
Acknowledgements Part of this work was done in the research project “Building a theorem-prover” at the Illinois Geometry Lab in Spring 2020. P.H. and C.S. were partially supported by NSF grant DMS-1654725. We thank Mary Angelica Gramcko-Tursi for carefully reading a draft of this paper.
Publisher Copyright:
© Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz, and Jeffrey Shallit.
PY - 2022/2/1
Y1 - 2022/2/1
N2 - 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.
AB - 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.
KW - Automated theorem proving
KW - Decidability
KW - Ostrowski numeration systems
KW - Sturmian words
UR - http://www.scopus.com/inward/record.url?scp=85124224105&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85124224105&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CSL.2022.24
DO - 10.4230/LIPIcs.CSL.2022.24
M3 - Conference contribution
AN - SCOPUS:85124224105
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 30th EACSL Annual Conference on Computer Science Logic, CSL 2022
A2 - Manea, Florin
A2 - Simpson, Alex
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 30th EACSL Annual Conference on Computer Science Logic, CSL 2022
Y2 - 14 February 2022 through 19 February 2022
ER -