Benutzer: Gast  Login
Dokumenttyp:
Technical Report 
Autor(en):
Steven Obua 
Titel:
Partizan Games in Isabelle/HOLZF 
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