Philipp Hieronymi ; Dun Ma ; Reed Oei ; Luke Schaeffer ; Christian Schulz et al. - Decidability for Sturmian words

lmcs:9980 - Logical Methods in Computer Science, August 5, 2024, Volume 20, Issue 3 - https://doi.org/10.46298/lmcs-20(3:12)2024
Decidability for Sturmian wordsArticle

Authors: Philipp Hieronymi ; Dun Ma ; Reed Oei ; Luke Schaeffer ; Christian Schulz ; Jeffrey Shallit

    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.


    Volume: Volume 20, Issue 3
    Published on: August 5, 2024
    Accepted on: February 8, 2024
    Submitted on: August 31, 2022
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Combinatorics,Mathematics - Logic

    Classifications

    Mathematics Subject Classification 20201

    Consultation statistics

    This page has been seen 1049 times.
    This article's PDF has been downloaded 412 times.