References
- Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8 17.
- Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.
- Yves Bertot. A short presentation of Coq. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics (TPHOLs 2008), volume 5170 of LNCS, pages 12–16. Springer, 2008. doi:10.1007/978-3-540-71067-7 3.
- Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development. Springer, 2004. ISBN 3540208542.
- John Horton Conway. On Numbers and Games. A K Peters Ltd., Natick, MA, second edition, 2001. ISBN 1-56881-127-6.
- Donald E. Knuth. Surreal Numbers: How Two Ex-students Turned on to Pure Mathematics and Found Total Happiness. Addison-Wesley, 1974.
- Lionel Elie Mamane. Surreal numbers in Coq. In Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors, Types for Proofs and Programs, TYPES 2004, volume 3839 of LNCS, pages 170–185. Springer, 2004. doi:10.1007/11617990 11.
- Tobias Nipkow and Gerwin Klein. Concrete Semantics: With Isabelle/HOL. Springer, 2014.
- Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL – A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. ISBN 3-540-43376-7.
- Steven Obua. Partizan games in Isabelle/HOLZF. In Kamel Barkaoui, Ana Cavalcanti, and Antonio Cerone, editors, Theoretical Aspects of Computing – ICTAC 2006, volume 4281 of LNCS, pages 272–286. Springer, 2006.
- Karol Pąk. Conway numbers – formal introduction. Formalized Mathematics, 31(1): 193–203, 2023. doi:10.2478/forma-2023-0018.
- Karol Pąk. Integration of game theoretic and tree theoretic approaches to Conway numbers. Formalized Mathematics, 31(1):205–213, 2023. doi:10.2478/forma-2023-0019.
- Karol Pąk. The ring of Conway numbers in Mizar. Formalized Mathematics, 31(1): 215–228, 2023. doi:10.2478/forma-2023-0020.
- Karol Pąk and Cezary Kaliszyk. Conway normal form: Bridging approaches for comprehensive formalization of surreal numbers. In Yves Bertot, Temur Kutsia, and Michael Norrish, editors, 15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia, volume 309 of LIPIcs, pages 29:1–29:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.ITP.2024.29.
- Dierk Schleicher and Michael Stoll. An introduction to Conway’s games and numbers. Moscow Mathematical Journal, 6:359–388, 2006. doi:10.17323/1609-4514-2006-6-2-359-388.
- Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The Isabelle framework. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, pages 33–38. Springer Berlin Heidelberg, 2008.
Language: English
Page range: 65 - 75
Accepted on: Oct 22, 2024
Published on: Nov 26, 2024
Published by: University of Białystok
In partnership with: Paradigm Publishing Services
Publication frequency: 1 issue per year
Keywords:
Related subjects:
© 2024 Karol Pąk, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.