User: Guest  Login
Title:

Partizan Games in Isabelle/HOLZF

Document type:
Technical Report
Author(s):
Steven Obua
Abstract:
Partizan Games (PGs) have been invented by John H. Conway and are described in his book On Numbers and Games. We formalize PGs in Higher Order Logic extended with ZF axioms (HOLZF) using Isabelle, a mechanical proof assistant. We show that PGs can be defined as the unique fixpoint of a function that arises naturally from Conway's original definition. While the construction of PGs in HOLZF relies heavily on the ZF axioms, operations on PGs are defined on a game type that hides its set theoretic o...     »
Keywords:
Higher Order Logic; Set Theory; Game Theory
Year:
2006
Year / month:
2006-05-01 00:00:00
Pages:
15
 BibTeX