# Positional Determinacy of Parity Games

 Title: Positional Determinacy of Parity Games Author: Christoph Dittmann Submission date: 2015-11-02 Abstract: We present a formalization of parity games (a two-player game on directed graphs) and a proof of their positional determinacy in Isabelle/HOL. This proof works for both finite and infinite games. BibTeX: @article{Parity_Game-AFP, author = {Christoph Dittmann}, title = {Positional Determinacy of Parity Games}, journal = {Archive of Formal Proofs}, month = nov, year = 2015, note = {\url{https://isa-afp.org/entries/Parity_Game.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Coinductive, Graph_Theory Used by: GaleStewart_Games 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.