Skip to main content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Erschienen 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

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, um Zugang zu erhalten
share
TEILEN

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.
Literatur
2.
5.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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
19.
22.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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)
Metadaten
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

Weitere Artikel der Ausgabe 8/2021

Journal of Automated Reasoning 8/2021 Zur Ausgabe

Premium Partner