A Symbolic Finite-state approach for Automated Proving of Theorems in Combinatorial Game Theory

TL;DR

This paper introduces a finite-state automata method implemented in Maple for conjecturing and rigorously proving theorems in combinatorial game theory, successfully resolving a conjecture in the Toads and Frogs game.

Contribution

It presents a novel automata-based approach and a Maple package for automated theorem proving in combinatorial games, including proof of a specific conjecture.

Findings

Automata approach effectively proves large families of positions.

Successfully proved Jeff Erickson's conjecture.

Provides a practical computational tool for combinatorial game analysis.

Abstract

We develop a finite-state automata approach, implemented in a Maple package {\tt ToadsAndFrogs} available from our websites, for conjecturing, and then rigorously proving, values for large families of positions in Richard Guy's combinatorial game ``Toads and Frogs''. In particular, we prove a conjecture of Jeff Erickson.