nach oben

Tipp

Formalization of Ring Theory in PVS

Isomorphism Theorems, Principal, Prime and Maximal Ideals, Chinese Remainder Theorem

verfasst von: Thaynara Arielly de Lima, André Luiz Galdino, Andréia Borges Avelar, Mauricio Ayala-Rincón

Erschienen in: Journal of Automated Reasoning | Ausgabe 8/2021

Einloggen

Abstract

This paper presents a PVS development of relevant results of the theory of rings. The PVS theory includes complete proofs of the three classical isomorphism theorems for rings, and characterizations of principal, prime and maximal ideals. Algebraic concepts and properties are specified and formalized as generally as possible allowing in this manner their application to other algebraic structures. The development provides the required elements to formalize important algebraic theorems. In particular, the paper presents the formalization of the general algebraic-theoretical version of the Chinese remainder theorem (CRT) for the theory of rings, as given in abstract algebra textbooks, proved as a consequence of the first isomorphism theorem. Also, the PVS theory includes a formalization of the number-theoretical version of CRT for the structure of integers, which is the version of CRT found in formalizations. CRT for integers is obtained as a consequence of the general version of CRT for the theory of rings.

Vorheriger Artikel Derivational Complexity and Context-Sensitive Rewriting

Nächster Artikel Experiences from Exporting Major Proof Assistant Libraries

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Available at https://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/.

Aransay, J., Ballarin, C., Baillon, M., de Vilhena, P.E., Hohe, S., Kammüller, F., Paulson, L.C.: The Isabelle/HOL Algebra Library. Technical report, Isabelle Library, University of Cambridge Computer Laboratory and Technische Universität München (2019). https://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/document.pdf

Artin, M.: Algebra, 2nd edn. Pearson, London (2010) MATH

Ayala-Rincón, M., de Moura, F.L.C.: Applied Logic for Computer Scientists: Computational Deduction and Formal Proofs. UTiCS. Springer (2017). https://doi.org/10.1007/978-3-319-51653-0

Ballarin, C.: Exploring the structure of an algebra text with locales. J. Autom. Reason. (2019). https://doi.org/10.1007/s10817-019-09537-9 CrossRefMATH

Bini, G., Flamini, F.: Finite Commutative Rings and Their Applications, vol. 680. Springer, Berlin (2012) MATH

Bourbaki, N.:Élèments de mathématique. Algèbre: chapitres 1 à 3. Springer, Berlin (2006). Réimpression inchangée de la 2e éd. 1970 Edition

Butler, R., Lester, D.: A PVS theory for abstract algebra (2007). http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html. Accessed 31 March 2019

Butler, R.W.: Formalization of the integral calculus in the PVS theorem prover. J. Formaliz. Reason. 2(1), 1–26 (2009). https://doi.org/10.6092/issn.1972-5787/1349 MathSciNetCrossRefMATH

Cano, G., Cohen, C., Dénès, M., Mörtberg, A., Siles, V.: Formalized linear algebra over elementary divisor rings in Coq. Log. Methods Comput. Sci. 12(2:7), 1–23 (2016). https://doi.org/10.2168/LMCS-12(2:7)2016 MathSciNetCrossRefMATH

10.

Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci. 8(1:2), 1–40 (2012). https://doi.org/10.2168/LMCS-8(1:2)2012 MathSciNetCrossRefMATH

11.

da Silva, A.B.A., de Lima, T.A., Galdino, A.L.: Formalizing ring theory in PVS. In: 9th International Conference on Interactive Theorem Proving ITP. Lecture Notes in Computer Science, vol. 10895, pp. 40–47. Springer (2018). https://doi.org/10.1007/978-3-319-94821-8_3

12.

Ding, C., Pei, D., Salomaa, A.: Chinese Remainder Theorem: Applications in Computing, Coding, Cryptography. World Scientific Publishing Co., Inc, River Edge (1996). https://doi.org/10.1142/3254 CrossRefMATH

13.

Dougherty, S., Leroy, A.F.A., Puczyłowski, E., Solé, P.: Noncommutative Rings and Their Applications. Contemporary Mathematics (2015). https://doi.org/10.1090/conm/634 CrossRef

14.

Dougherty, S., Leroy, A.: Euclidean self-dual codes over non-commutative Frobenius rings. Appl. Algebra Eng. Commun. Comput. 27(3), 185–203 (2016). https://doi.org/10.1007/s00200-015-0277-0 MathSciNetCrossRefMATH

15.

Dummit, D.S., Foote, R.M.: Abstract Algebra, 3rd edn. Wiley, Hoboken (2003) MATH

16.

Galdino, A.L., Ayala-Rincón, M.: A PVS theory for term rewriting systems. Electron. Notes Theor. Comput. Sci. 247, 67–83 (2009). https://doi.org/10.1016/j.entcs.2009.07.049 MathSciNetCrossRefMATH

17.

Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: A constructive algebraic hierarchy in Coq. J. Symb. Comput. 34(4), 271–286 (2002). https://doi.org/10.1006/jsco.2002.0552 MathSciNetCrossRefMATH

18.

Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O’Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L.: A machine-checked proof of the odd order theorem. In: 4th International Conference on Interactive Theorem Proving ITP. Lecture Notes in Computer Science, vol. 7998, pp. 163–179. Springer (2013). https://doi.org/10.1007/978-3-642-39634-2_14

19.

Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Théry, L.: A modular formalisation of finite group theory. In: 20th International Conference Theorem Proving in Higher Order Logics TPHOLs. Lecture Notes in Computer Science, vol. 4732, pp. 86–101. Springer (2007). https://doi.org/10.1007/978-3-540-74591-4_8

20.

Großschädl, J.: The Chinese remainder theorem and its application in a high-speed RSA crypto chip. In: 16th Annual Computer Security Applications Conference ACSAC, pp. 384–393. IEEE Computer Society (2000). https://doi.org/10.1109/ACSAC.2000.898893

21.

Heras, J., Martín-Mateos, F.J., Pascual, V.: Modelling algebraic structures and morphisms in ACL2. Appl. Algebra Eng. Commun. Comput. 26(3), 277–303 (2015). https://doi.org/10.1007/s00200-015-0252-9 MathSciNetCrossRefMATH

22.

Herstein, I.N.: Topics in Algebra, 2nd edn. Xerox College Publishing, Lexington (1975) MATH

23.

Hungerford, T.W.: Algebra. Graduate Texts in Mathematics, vol. 73. Springer, New York (1980). (Reprint of the 1974 original)

24.

Jackson, P.B.: Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. Ph.D. thesis, Cornell University (1995)

25.

Jacobson, N.: Basic Algebra I. Dover Books on Mathematics, 2nd edn. Dover Publications, Mineola (2009)

26.

Kornilowicz, A., Schwarzweller, C.: The first isomorphism theorem and other properties of rings. Formaliz. Math. 22(4), 291–301 (2014). https://doi.org/10.2478/forma-2014-0029 CrossRefMATH

27.

Lester, D.: A PVS Theory for Continuity, Homeomorphisms, Connected and Compact Spaces, Borel Sets/Functions (2009). http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html. Accessed 31 March 2019

28.

Liang, H., Li, X., Xia, X.: Adaptive frequency estimation with low sampling rates based on robust Chinese remainder theorem and IIR notch filter. Adv. Adapt. Data Anal. 1(4), 587–600 (2009). https://doi.org/10.1142/S1793536909000230 MathSciNetCrossRef

29.

Lidl, R., Niederreiter, H.: Introduction to Finite Fields and Their Applications. Cambridge University Press, Cambridge (1994) CrossRef

30.

Noether, E.: Abstrakter Aufbau der Idealtheorie in algebraischen Zahl- und Funktionenkörpern. Mathematische Annalen 96(1), 26–61 (1927) MathSciNetCrossRef

31.

Owre, S., Shankar, N.: The Formal Semantics of PVS. Technical Report 97-2R, SRI International Computer Science Laboratory, Menlo Park (1997) (revised 1999)

32.

Philipoom, J.: Correct-by-Construction Finite Field Arithmetic in Coq. Master’s thesis, Master of Engineering in Computer Science, MIT (2018)

33.

Putinar, M., Sullivant, S.: Emerging Applications of Algebraic Geometry. The IMA Volumes in Mathematics and its Applications. Springer, New York (2008). https://doi.org/10.1007/978-0-387-09686-5

34.

Russinoff, D.M.: A Mechanical Proof of the Chinese Remainder Theorem. UTCS Technical Report-no longer available-ACL2 Workshop 2000 TR-00-29, University of Texas at Austin (2000)

35.

Schwarzweller, C.: The binomial theorem for algebraic structures. J. Formaliz. Math. 12(3), 559–564 (2003)

36.

Schwarzweller, C.: The Chinese remainder theorem, its proofs and its generalizations in mathematical repositories. Stud. Log. Gramm. Rhetor. 18(31), 103–119 (2009)

37.

Suárez, Y.G., Torres, E., Pereira, O., Pérez, C., Rodríguez, R.: Application of the ring theory in the segmentation of digital images. Int. J. Soft Comput. Math. Control 3(4), 69–81 (2014). https://doi.org/10.14810/ijscmc.2014.3405 CrossRef

38.

The mathlib Community.: The Lean Mathematical Library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367–381. ACM (2020). https://doi.org/10.1145/3372885.3373824

39.

van der Waerden, B.L.: Algebra, vol. I. Springer, New York (1991) CrossRef

40.

Walther, C.: A Machine Assisted Proof of the Chinese Remainder Theorem. Technical Report VFR 18/03, FB Informatik, Technische Universität Darmstadt (2018)

41.

Zhang, H., Hua, X.: Proving the Chinese remainder theorem by the cover set induction. In: 11th International Conference on Automated Deduction CADE. Lecture Notes in Computer Science, vol. 607, pp. 431–445. Springer (1992). https://doi.org/10.1007/3-540-55602-8_182

Titel: Formalization of Ring Theory in PVS
Isomorphism Theorems, Principal, Prime and Maximal Ideals, Chinese Remainder Theorem
verfasst von: Thaynara Arielly de Lima
André Luiz Galdino
Andréia Borges Avelar
Mauricio Ayala-Rincón
Publikationsdatum: 12.05.2021
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 8/2021
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-021-09593-0

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 8/2021

Experiences from Exporting Major Proof Assistant Libraries

Human-Centered Automated Proof Search

Derivational Complexity and Context-Sensitive Rewriting

An Automatically Verified Prototype of the Tokeneer ID Station Specification

Handling Transitive Relations in First-Order Automated Reasoning