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

arXiv: https://arxiv.org/abs/2209.03266 · HTML: https://mlsanity.com/paper/2209.03266/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Sep 2022.

## Built on by (most cited first, 1 of 1)

- [Deconstructing Subset Construction -- Reducing While Determinizing](https://mlsanity.com/paper/2505.10319/) (2025)

## Abstract (arXiv)

We show that the first-order logical theory of the binary overlap-free words (and, more generally, the α-free words for rational α, 2 < α ≤ 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.