@ARTICLE{SURREALR.MIZ,
  AUTHOR = {P\k{a}k, Karol},
  TITLE = {The Ring of {C}onway Numbers in {M}izar},
  SECTION1 = {Preliminaries},
  SECTION2 = {Surreal Number Operators -- Schemes},
  SECTION3 = {The Opposite Surreal Number},
  SECTION4 = {The Sum of Surreal Numbers},
  SECTION5 = {The Product of Superreal Numbers},
  DAY = {12},
  MONTH = {December},
  YEAR = {2023},
  ADDRESS1 = {Faculty of Computer Science\\University of Bia{\l}ystok\\ Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {Conway's introduction to algebraic operations on surreal numbers 
  with a rather simple definition. However, he combines recursion with Conway's induction on   surreal numbers, more formally he combines 
  transfinite induction-recursion with the properties of proper classes,
  which is difficult to introduce formally.\par
  This article represents a further step in our ongoing efforts to 
  investigate the possibilities offered by Mizar with Tarski-Grotendieck set 
  theory \cite{CBKP-CICM/MKM19} to introduce the algebraic 
  structure of Conway numbers \cite{SURREAL0} and to prove their ring character.\par
  The formalisation is mainly based on \cite{Conway:2001}, but also 
  uses selected ideas proposed in \cite{alabdullah,Alling,schleicher}.
  We formalised four sections, namely
  {\it Properties of Addition}, {\it Properties of Negation}, 
  {\it Properties of Addition and Order} and {\it Properties of Multiplication}
  in  Chapter 1 of John Conway's seminal book.}}

@inproceedings{CBKP-CICM/MKM19,
  author    = {Brown, Chad E. and Karol P\k{a}k},
  editor    = {Kaliszyk, Cezary and 
               Brady, Edwin and 
               Kohlhase, Andrea and 
               Sacerdoti Coen, Claudio},
  title     = {A Tale of Two Set Theories},
  booktitle = {Intelligent Computer Mathematics - 12th International Conference,
               {CICM} 2019, CIIRC, Prague, Czech Republic, July 8-12, 2019, Proceedings},
  series    = {Lecture Notes in Computer Science},
  pages     = {44--60},
  year      = {2019},
  volume    = {11617},
  publisher = {Springer},
  doi       = {10.1007/978-3-030-23250-4_4}
}
