Mechanical Proofs of Properties of the Tribonacci Word

TL;DR

This paper develops a decision procedure to analyze properties of the Tribonacci word, enabling reproof of known results and discovery of new properties related to its structure and repetitions.

Contribution

It introduces a novel decision procedure for Tribonacci-automatic words, allowing automated proofs and new findings about their combinatorial properties.

Findings

Reproved known results about squares, cubes, and palindromes in the Tribonacci word

Discovered new structural properties of the Tribonacci word

Established a framework for automated reasoning about Tribonacci-automatic sequences

Abstract

We implement a decision procedure for answering questions about a class of infinite words that might be called (for lack of a better name) "Tribonacci-automatic". This class includes, for example, the famous Tribonacci word T = 0102010010202 ..., the fixed point of the morphism 0 -> 01, 1 -> 02, 2 -> 0. We use it to reprove some old results about the Tribonacci word from the literature, such as assertions about the occurrences in T of squares, cubes, palindromes, and so forth. We also obtain some new results.