Logo PTI Logo FedCSIS

Proceedings of the 18th Conference on Computer Science and Intelligence Systems

Annals of Computer Science and Information Systems, Volume 35

Developing Field Theory in Mizar

DOI: http://dx.doi.org/10.15439/2023F3409

Citation: Proceedings of the 18th Conference on Computer Science and Intelligence Systems, M. Ganzha, L. Maciaszek, M. Paprzycki, D. Ślęzak (eds). ACSIS, Vol. 35, pages 303–308 ()

Full text

Abstract. 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.

References

  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.