Inverse Element for Surreal Number

Pole DC	Wartość	Język
dc.contributor.author	Pąk, Karol	-
dc.date.accessioned	2024-12-10T08:57:58Z	-
dc.date.available	2024-12-10T08:57:58Z	-
dc.date.issued	2024	-
dc.identifier.citation	Formalized Mathematics, Volume 32, Issue 1, Pages 65–75	pl
dc.identifier.issn	1426-2630	-
dc.identifier.uri	http://hdl.handle.net/11320/17712	-
dc.description.abstract	Conway’s surreal numbers have a fascinating algebraic structure, which we try to formalise in the Mizar system. In this article, building on our previous work establishing that the surreal numbers fulfil the ring properties, we construct the inverse element for any non-zero number. For that purpose, we formalise the definition of the inverse element formulated in Section Properties of Division of Conway’s book. In this way we show formally in the Mizar system that surreal numbers satisfy all nine properties of a field.	pl
dc.language.iso	en	pl
dc.publisher	DeGruyter Open	pl
dc.rights	Attribution-ShareAlike 3.0 Unported (CC BY-SA 3.0)	pl
dc.rights.uri	https://creativecommons.org/licenses/by-sa/3.0/	pl
dc.subject	surreal numbers	pl
dc.subject	Conway’s game	pl
dc.title	Inverse Element for Surreal Number	pl
dc.type	Article	pl
dc.rights.holder	© 2024 The Author(s)	pl
dc.rights.holder	CC BY-SA 3.0 license	pl
dc.identifier.doi	10.2478/forma-2024-0005	-
dc.description.Affiliation	Faculty of Computer Science, University of Białystok, Poland	pl
dc.description.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-3319-20614-1. doi:10.1007/978-3-319-20615-8_17.	pl
dc.description.references	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.	pl
dc.description.references	Yves Bertot. A short presentation of Coq. In Otmane Aït Mohamed, César A. Munoz, 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.	pl
dc.description.references	Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development. Springer, 2004. ISBN 3540208542.	pl
dc.description.references	John Horton Conway. On Numbers and Games. A K Peters Ltd., Natick, MA, second edition, 2001. ISBN 1-56881-127-6.	pl
dc.description.references	Donald E. Knuth. Surreal Numbers: How Two Ex-students Turned on to Pure Mathematics and Found Total Happiness. Addison-Wesley, 1974.	pl
dc.description.references	Lionel Elie Mamane. Surreal numbers in Coq. In Jean-Christophe Filliˆatre, 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.	pl
dc.description.references	Tobias Nipkow and Gerwin Klein. Concrete Semantics: With Isabelle/HOL. Springer, 2014.	pl
dc.description.references	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.	pl
dc.description.references	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.	pl
dc.description.references	Karol Pąk. Conway numbers– formal introduction. Formalized Mathematics, 31(1): 193–203, 2023. doi:10.2478/forma-2023-0018.	pl
dc.description.references	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.	pl
dc.description.references	Karol Pąk. The ring of Conway numbers in Mizar. Formalized Mathematics, 31(1): 215–228, 2023. doi:10.2478/forma-2023-0020.	pl
dc.description.references	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¨ ur Informatik, 2024. doi:10.4230/LIPICS.ITP.2024.29.	pl
dc.description.references	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.	pl
dc.description.references	Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The Isabelle framework. In Otmane Ait Mohamed, C´esar Mu˜noz, and Sofi` ene Tahar, editors, Theorem Proving in Higher Order Logics, pages 33–38. Springer Berlin Heidelberg, 2008.	pl
dc.identifier.eissn	1898-9934	-
dc.description.volume	32	pl
dc.description.issue	1	pl
dc.description.firstpage	65	pl
dc.description.lastpage	75	pl
dc.identifier.citation2	Formalized Mathematics	pl
dc.identifier.orcid	0000-0002-7099-1669	-
Występuje w kolekcji(ach):	Artykuły naukowe (WInf) Formalized Mathematics, 2024, Volume 32, Issue 1

Pliki w tej pozycji:

Plik	Opis	Rozmiar	Format
Inverse-Element-for-Surreal-Number.pdf		310,73 kB	Adobe PDF	Otwórz

Pokaż uproszczony widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL