Benutzer: Gast  Login
Titel:

Partizan Games in Isabelle/HOLZF

Dokumenttyp:
Technical Report
Autor(en):
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...     »
Stichworte:
Higher Order Logic; Set Theory; Game Theory
Jahr:
2006
Jahr / Monat:
2006-05-01 00:00:00
Seiten/Umfang:
15
 BibTeX