Combinatorial game theory; Automatic proof; Walnut; Büchi theorem
Abstract :
[en] The Büchi–Bruyère theorem asserts that the first-order theory of certain extensions of Pres-
burger arithmetic is decidable. The software Walnut implements the corresponding transformation of first-order formulas into automata. This tool has already been widely and successfully used in combinatorics on words to automatically reprove results from the literature as well as proving new results. We present a new range of applications of the tool in combinatorial game theory. This is the first time this tool and such a formalism have been applied in the context of games as far as we know.
We consider Wythoff’s game and many variations studied by Fraenkel and others. In this
paper, we show how to use Walnut to obtain short automatic proofs of several results from the literature. We also prove a conjecture stated by Duchêne et al. regarding additional moves not changing the set of the P-positions of Wythoff’s game. We further state some new conjectures related to redundant moves. This work is linked with non-standard numeration systems for which addition is recognizable by a finite automaton.
