Decidability for Sturmian Words

Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz, Jeffrey Shallit

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publication30th EACSL Annual Conference on Computer Science Logic, CSL 2022
EditorsFlorin Manea, Alex Simpson
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959772181
StatePublished - Feb 1 2022
Event30th EACSL Annual Conference on Computer Science Logic, CSL 2022 - Virtual, Gottingen, Germany
Duration: Feb 14 2022Feb 19 2022

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
ISSN (Print)1868-8969


Conference30th EACSL Annual Conference on Computer Science Logic, CSL 2022
CityVirtual, Gottingen


  • Automated theorem proving
  • Decidability
  • Ostrowski numeration systems
  • Sturmian words

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Decidability for Sturmian Words'. Together they form a unique fingerprint.

Cite this