Mechanical proving with Walnut for squares and cubes in partial words

TL;DR

This paper demonstrates how Walnut automata can be used to prove theorems about avoiding squares and cubes in partial words, introduces the concept of antisquares, and explores binary partial words with limited squares and antisquares.

Contribution

It applies Walnut to new and existing results on partial words, introduces antisquares, and initiates the study of binary partial words with constrained square and antisquare counts.

Findings

Walnut successfully proves new and old results on avoiding repetitions in partial words.

Introduces the concept of antisquares in partial words.

Begins analysis of binary partial words with limited squares and antisquares.

Abstract

Walnut is a software that using automata can prove theorems in combinatorics on words about automatic sequences. We are able to apply this software to both prove new results as well as reprove some old results on avoiding squares and cubes in partial words. We also define the notion of an antisquare in a partial word and begin the study of binary partial words which contain only a fixed number of distinct squares and antisquares.