[Club2] Vortrag am 23.02.05

[Norbert Schirmer]

This week:

16:30 - 17:30h, in Room 00.09.055 (Alan Turing). 

Steven Obua: Constructing Partizan Games in Isabelle/HOL-ZF 

Abstract: 


Partizan games are the games that Conway considers in his book "On Numbers and 
Games". They are a prerequisite for constructing his surreal numbers. In this 
talk we first define what we mean by Isabelle/HOL-ZF. We then define Partizan 
Games as a fixpoint of a function that corresponds to the definition that 
Conway gave in his book, and show that there is a unique such fixpoint. 



   Norbert