Top

Journal of Automated Reasoning

Published in:

12-05-2021

Formalization of Ring Theory in PVS

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

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

Published in: Journal of Automated Reasoning | Issue 8/2021

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

previous article Derivational Complexity and Context-Sensitive Rewriting

next article Experiences from Exporting Major Proof Assistant Libraries

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

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-9CrossRefMATH

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/1349MathSciNetCrossRefMATH

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)2016MathSciNetCrossRefMATH

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)2012MathSciNetCrossRefMATH

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/3254CrossRefMATH

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/634CrossRef

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-0MathSciNetCrossRefMATH

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.049MathSciNetCrossRefMATH

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.0552MathSciNetCrossRefMATH

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-9MathSciNetCrossRefMATH

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-0029CrossRefMATH

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/S1793536909000230MathSciNetCrossRef

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.3405CrossRef

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

Title: Formalization of Ring Theory in PVS
Isomorphism Theorems, Principal, Prime and Maximal Ideals, Chinese Remainder Theorem
Authors: Thaynara Arielly de Lima
André Luiz Galdino
Andréia Borges Avelar
Mauricio Ayala-Rincón
Publication date: 12-05-2021
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 8/2021
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-021-09593-0

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 8/2021

An Automatically Verified Prototype of the Tokeneer ID Station Specification

Handling Transitive Relations in First-Order Automated Reasoning

Experiences from Exporting Major Proof Assistant Libraries

Human-Centered Automated Proof Search

Derivational Complexity and Context-Sensitive Rewriting

Premium Partner