Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem

DOI10.1007/s10817-021-09593-0zbMath1493.68389OpenAlexW3163136021WikidataQ113901238 ScholiaQ113901238MaRDI QIDQ2069874

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

Publication date: 21 January 2022

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-021-09593-0

zbMATH Keywords

maximal idealsprime idealsprincipal idealsring theoryisomorphism theoremsPVSChinese remainder theorem for rings

Mathematics Subject Classification ID

Computational aspects and applications of commutative rings (13P99) Mechanization of proofs and logical operations (03B35) Computational aspects of associative rings (general theory) (16Z05) Sets with a single binary operation (groupoids) (20N02) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

A formalization of Dedekind domains and class groups of global fields

Uses Software

• Isabelle
• PVS
• mathlib

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Euclidean self-dual codes over non-commutative Frobenius rings
• A constructive algebraic hierarchy in Coq.
• Applied logic for computer scientists. Computational deduction and formal proofs
• Formalizing ring theory in PVS
• Exploring the structure of an algebra text with locales
• Modelling algebraic structures and morphisms in ACL2
• The first isomorphism theorem and other properties of rings
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• A Modular Formalisation of Finite Group Theory
• A Brief Overview of PVS
• Noncommutative Rings and Their Applications
• A PVS Theory for Term Rewriting Systems
• A Machine-Checked Proof of the Odd Order Theorem
• Formalized linear algebra over Elementary Divisor Rings in Coq
• Algèbre commutative

This page was built for publication: Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem