The First-Order Theory of Binary Overlap-Free Words is Decidable

TL;DR

This paper proves that the first-order logical theory of binary overlap-free words and related classes is decidable, enabling automatic verification of many properties previously proven through complex case analysis.

Contribution

It establishes the decidability of the first-order theory for binary overlap-free words and generalizes to certain alpha-free words, simplifying proofs of their properties.

Findings

Decidability of the first-order theory for binary overlap-free words.

Automated proof of properties previously proven manually.

Extension of results to alpha-free words for 2 < alpha ≤ 7/3.

Abstract

We show that the first-order logical theory of the binary overlap-free words (and, more generally, the ${\alpha}$-free words for rational ${\alpha}$, $2 < {\alpha} \leq 7/3$), is decidable. As a consequence, many results previously obtained about this class through tedious case- based proofs can now be proved "automatically", using a decision procedure.