Automatic proofs in combinatorial game theory

Bastien Mignoty, Antoine Renard (), Michel Rigo () and Markus A. Whiteland ()
Additional contact information
Bastien Mignoty: ENS Lyon
Antoine Renard: University of Liège
Michel Rigo: University of Liège
Markus A. Whiteland: Loughborough University

International Journal of Game Theory, 2025, vol. 54, issue 2, No 10, 32 pages

Abstract: Abstract The Büchi–Bruyère theorem asserts that the first-order theory of certain extensions of Presburger 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 $${\mathcal {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.

Keywords: Combinatorial game theory; Wythoff’s game; Automatic theorem proving; Numeration systems; First-order logic; 91A46; 91A05; 68V15; 68Q45; 11A67 (search for similar items in EconPapers)
Date: 2025
References: Add references at CitEc
Citations:

Downloads: (external link)
http://link.springer.com/10.1007/s00182-025-00953-3 Abstract (text/html)
Access to the full text of the articles in this series is restricted.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:jogath:v:54:y:2025:i:2:d:10.1007_s00182-025-00953-3

Ordering information: This journal article can be ordered from
http://www.springer. ... eory/journal/182/PS2

DOI: 10.1007/s00182-025-00953-3

Access Statistics for this article

International Journal of Game Theory is currently edited by Shmuel Zamir, Vijay Krishna and Bernhard von Stengel

More articles in International Journal of Game Theory from Springer, Game Theory Society
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().