|
Gale-Stewart
Games
Title: |
Gale-Stewart Games |
Author:
|
Sebastiaan Joosten
|
Submission date: |
2021-04-23 |
Abstract: |
This is a formalisation of the main result of Gale and Stewart from
1953, showing that closed finite games are determined. This property
is now known as the Gale Stewart Theorem. While the original paper
shows some additional theorems as well, we only formalize this main
result, but do so in a somewhat general way. We formalize games of a
fixed arbitrary length, including infinite length, using co-inductive
lists, and show that defensive strategies exist unless the other
player is winning. For closed games, defensive strategies are winning
for the closed player, proving that such games are determined. For
finite games, which are a special case in our formalisation, all games
are closed. |
BibTeX: |
@article{GaleStewart_Games-AFP,
author = {Sebastiaan Joosten},
title = {Gale-Stewart Games},
journal = {Archive of Formal Proofs},
month = apr,
year = 2021,
note = {\url{https://isa-afp.org/entries/GaleStewart_Games.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Parity_Game |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|