Developing Field Theory in Mizar

• Autorzy: Schwarzweller Christoph

Identyfikatory

DOI

10.15439/2023F3409

• Języki publikacji: EN

Abstrakty

EN

As part of our ongoing project to prove Artin's solution of Hilbert's 17th problem in Mizar we are formalizing a great deal of basic field and Galois theory. In this paper we report on our formalization so far: we present basic mathematical structures and our Mizar definitions enriched with some main results. We also discuss some our design decisions as well as subtleties, in particular connected with Mizar types.

Słowa kluczowe

EN

isomorphism; vector space; group theory; finite field; monomorphism

PL

izomorfizm; przestrzeń wektorowa; teoria grup; pole skończone; monomorfizm

• Wydawca: Polskie Towarzystwo Informatyczne
• Czasopismo: Annals of Computer Science and Information Systems
• Rocznik: 2023
• Tom: Vol. 35
• Strony: 303--308
• Opis fizyczny: Bibliogr. 23 poz., wz.

Twórcy

autor

Schwarzweller Christoph

• Institute of Informatics, Faculty of Mathematics, Physics and Informatics, University of Gdańsk, Wita Stwosza 57, 80-952 Gdańsk, Poland

Bibliografia

• 1. E. Artin, Über die Zerlegung definiter Funktionen in Quadrate; Abh. Math. Sem. Univ. Hamburg 5(1), pp. 100–115, 1927.
• 2. G. Bancerek et.al., Mizar: State-of-the-art and Beyond. in: M. Kerber et.al. (eds.), Proceedings of the 2015 International Conference on Intelligent Computer Mathematics, Lecture Notes in Computer Science 9150, 261–279, 2015. http://dx.doi.org/10.1007/978-3-319-20615-8_17
• 3. G. Bancerek, C. Bylinski, A. Grabowski, A. Kornilowicz, R. Matuszewski, A. Naumowic, and K. Pak, The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar; Journal of Automated Reasoning, vol. 61(1-4), pp. 9–32, 2018.
• 4. S. Bernard, C. Cohen, and A. Mahboubi and P. Strub, Unsolvability of the Quintic Formalized in Dependent Type Theory, available at https://hal.inria.fr/hal-03136002, 2021.
• 5. T. Browning and P. Lutz, Formalizing Galois Theory; Experimental Mathematics, vol. 31(2), pp. 413–424 2022.
• 6. C. Cohen, Construction of Real Algebraic Numbers in Coq, in: ITP - 3rd International Conference on Interactive Theorem Proving, pp. 67–82, 2012.
• 7. The Coq Proof Assistant. available at www.coq.inria.fr.
• 8. P.E. de Vilhena and L.C. Paulson, Algebraically Closed Fields in Isabelle/HOL in: Automated Reasoning. IJCAR 2020, Lecture Notes in Computer Science 12167, pp. 57–64, 2020.
• 9. A. Gathmann, Einführung in die Algebra; Lecture notes, University of Kaiserslautern, Germany, 2010.
• 10. A. Grabowski, R. Coghetto Topological structures as a tool for formal modelling of rough sets; Position Papers of the 2017 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 12, pp. 11-18, 2017.
• 11. A. Grabowski, A. Korniłowicz, and A. Naumowicz, Mizar in a Nutshell. Journal of Formalized Reasoning 3(2), 153–245, 2010. https://doi.org/10.6092/issn.1972-5787/1980
• 12. A. Grabowski, A. Korniłowicz, and C. Schwarzweller, On Algebraic Hierarchies in Mathematical Repository of Mizar. in: Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 8, 363–371, 2016. http://dx.doi.org/10.15439/2016F520
• 13. A. Grabowski, A. Korniłowicz, and A. Naumowicz, Four Decades of Mizar. Journal of Automated Reasoning, vol 55(3), 191–198, 2015. http://dx.doi.org/10.1007/s10817-015-9345-1
• 14. J. Harrison, The HOL Light Theorem Prover. available at www.cl.cam.ac.uk/~jrh13/hol-light.
• 15. The HOL Interactive Theorem Prover. available at hol-theorem-prover. org.
• 16. Isabelle. available at isabelle.in.tum.de.
• 17. S. Lang, Algebra, 3rd edition, Springer Verlag, 2002.
• 18. Mizar Home Page. available at www.mizar.org.
• 19. A. Naumowicz and A. Korniłowicz, A Brief Overview of Mizar. in: Theorem Proving in Higher Order Logics 2009, S. Berghofer, T. Nipkow, C. Urban, M. Wenzel (eds.), Lecture Notes in Computer Science, 5674, 67–72, Springer Verlag, 2009.
• 20. K. Pak, Formalization of the MRDP-Theorem in the Mizar System, Formalized Mathematics, vol. 27(2), pp. 209–222, 2019.
• 21. K. Radbruch, Algebra I; Lecture notes, University of Kaiserslautern, Germany, 1990.
• 22. K. Radbruch, Geordnete Körper; Lecture notes, University of Kaiserslautern, Germany, 1991.
• 23. C. Schwarzweller Representation Matters: An Unexpected Property of Polynomial Rings and its Consequences for Formalizing Abstract Field Theory; in: M. Ganzha, L. Maciaszek, M. Paprzycki (eds.), Proceedings of the 2018 Federated Conference on Computer Science and Information Systems, ACSIS, vol. 15, pp. 67-72, 2018.

Uwagi

1. Main Track Short Papers

2. Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2024).