1 Search Results for "Ma, Dun"

Document
DOI: 10.4230/LIPIcs.CSL.2022.24
Decidability for Sturmian Words

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

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
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.
Cite as

Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz, and Jeffrey Shallit. Decidability for Sturmian Words. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 24:1-24:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{hieronymi_et_al:LIPIcs.CSL.2022.24,
  author =	{Hieronymi, Philipp and Ma, Dun and Oei, Reed and Schaeffer, Luke and Schulz, Christian and Shallit, Jeffrey},
  title =	{{Decidability for Sturmian Words}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{24:1--24:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.24},
  URN =		{urn:nbn:de:0030-drops-157440},
  doi =		{10.4230/LIPIcs.CSL.2022.24},
  annote =	{Keywords: Decidability, Sturmian words, Ostrowski numeration systems, Automated theorem proving}
}
  • Refine by Author
  • 1 Hieronymi, Philipp
  • 1 Ma, Dun
  • 1 Oei, Reed
  • 1 Schaeffer, Luke
  • 1 Schulz, Christian
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 Automated theorem proving
  • 1 Decidability
  • 1 Ostrowski numeration systems
  • 1 Sturmian words

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact