Skip to main content
main-content
Top

Hint

Swipe to navigate through the articles of this issue

Published in: Journal of Automated Reasoning 8/2021

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

Login to get access
share
SHARE

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.
Literature
2.
5.
go back to reference Bini, G., Flamini, F.: Finite Commutative Rings and Their Applications, vol. 680. Springer, Berlin (2012) MATH Bini, G., Flamini, F.: Finite Commutative Rings and Their Applications, vol. 680. Springer, Berlin (2012) MATH
6.
go back to reference 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 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
15.
go back to reference Dummit, D.S., Foote, R.M.: Abstract Algebra, 3rd edn. Wiley, Hoboken (2003) MATH Dummit, D.S., Foote, R.M.: Abstract Algebra, 3rd edn. Wiley, Hoboken (2003) MATH
18.
go back to reference 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 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
22.
go back to reference Herstein, I.N.: Topics in Algebra, 2nd edn. Xerox College Publishing, Lexington (1975) MATH Herstein, I.N.: Topics in Algebra, 2nd edn. Xerox College Publishing, Lexington (1975) MATH
23.
go back to reference Hungerford, T.W.: Algebra. Graduate Texts in Mathematics, vol. 73. Springer, New York (1980). (Reprint of the 1974 original) Hungerford, T.W.: Algebra. Graduate Texts in Mathematics, vol. 73. Springer, New York (1980). (Reprint of the 1974 original)
24.
go back to reference Jackson, P.B.: Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. Ph.D. thesis, Cornell University (1995) Jackson, P.B.: Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. Ph.D. thesis, Cornell University (1995)
25.
go back to reference Jacobson, N.: Basic Algebra I. Dover Books on Mathematics, 2nd edn. Dover Publications, Mineola (2009) Jacobson, N.: Basic Algebra I. Dover Books on Mathematics, 2nd edn. Dover Publications, Mineola (2009)
29.
go back to reference Lidl, R., Niederreiter, H.: Introduction to Finite Fields and Their Applications. Cambridge University Press, Cambridge (1994) CrossRef Lidl, R., Niederreiter, H.: Introduction to Finite Fields and Their Applications. Cambridge University Press, Cambridge (1994) CrossRef
30.
go back to reference Noether, E.: Abstrakter Aufbau der Idealtheorie in algebraischen Zahl- und Funktionenkörpern. Mathematische Annalen 96(1), 26–61 (1927) MathSciNetCrossRef Noether, E.: Abstrakter Aufbau der Idealtheorie in algebraischen Zahl- und Funktionenkörpern. Mathematische Annalen 96(1), 26–61 (1927) MathSciNetCrossRef
31.
go back to reference Owre, S., Shankar, N.: The Formal Semantics of PVS. Technical Report 97-2R, SRI International Computer Science Laboratory, Menlo Park (1997) (revised 1999) Owre, S., Shankar, N.: The Formal Semantics of PVS. Technical Report 97-2R, SRI International Computer Science Laboratory, Menlo Park (1997) (revised 1999)
32.
go back to reference Philipoom, J.: Correct-by-Construction Finite Field Arithmetic in Coq. Master’s thesis, Master of Engineering in Computer Science, MIT (2018) Philipoom, J.: Correct-by-Construction Finite Field Arithmetic in Coq. Master’s thesis, Master of Engineering in Computer Science, MIT (2018)
34.
go back to reference 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) 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.
go back to reference Schwarzweller, C.: The binomial theorem for algebraic structures. J. Formaliz. Math. 12(3), 559–564 (2003) Schwarzweller, C.: The binomial theorem for algebraic structures. J. Formaliz. Math. 12(3), 559–564 (2003)
36.
go back to reference Schwarzweller, C.: The Chinese remainder theorem, its proofs and its generalizations in mathematical repositories. Stud. Log. Gramm. Rhetor. 18(31), 103–119 (2009) Schwarzweller, C.: The Chinese remainder theorem, its proofs and its generalizations in mathematical repositories. Stud. Log. Gramm. Rhetor. 18(31), 103–119 (2009)
39.
40.
go back to reference Walther, C.: A Machine Assisted Proof of the Chinese Remainder Theorem. Technical Report VFR 18/03, FB Informatik, Technische Universität Darmstadt (2018) Walther, C.: A Machine Assisted Proof of the Chinese Remainder Theorem. Technical Report VFR 18/03, FB Informatik, Technische Universität Darmstadt (2018)
Metadata
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

Other articles of this Issue 8/2021

Journal of Automated Reasoning 8/2021 Go to the issue

Premium Partner