A formalization of the Smith normal form in higher-order logic

DOI10.1007/s10817-022-09631-5OpenAlexW4281558819MaRDI QIDQ2102950

Jose Divasón, René Thiemann

Publication date: 12 December 2022

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

Full work available at URL: https://doi.org/10.1007/s10817-022-09631-5

zbMATH Keywords

theorem provingIsabelle/HOLelementary divisor ringslocal type definitions

Mathematics Subject Classification ID

Matrices over special rings (quaternions, finite fields, etc.) (15B33) Principal ideal rings (13F10) Canonical forms, reductions, classification (15A21) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• ACL2
• Coq
• Isabelle
• Isabelle/HOL
• PVS
• Mizar
• Kenzo
• HOL Light
• Locales
• Transfer
• Lifting
• MathOverflow
• Echelon Form
• Cayley-Hamilton
• Berlekamp Zassenhaus
• Archive Formal Proofs
• Modular_arithmetic_LLL_and_HNF_algorithms
• Smith_Normal_Form
• Hermite
• Smooth_Manifolds

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Commutative algebra in the Mizar system
• Smith normal form in combinatorics
• Some remarks on elementary divisor rings. II
• Isabelle/HOL. A proof assistant for higher-order logic
• From types to sets by local type definition in higher-order logic
• Formalizing ring theory in PVS
• The HOL Light theory of Euclidean space
• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
• A generic and executable formalization of signature-based Gröbner basis algorithms
• Exploring the structure of an algebra text with locales
• Locales: a module system for mathematical theories
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• A bijective proof of Muir's identity and the Cauchy-Binet formula
• A Refinement-Based Approach to Computational Algebra in Coq
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Some Remarks About Elementary Divisor Rings
• Mining the Archive of Formal Proofs
• Application of the Smith Normal Form to the Structure of Lattice Rules
• A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
• Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
• Theorem Proving in Higher Order Logics
• Algorithms for Hermite and Smith Normal Matrices and Linear Diophantine Equations
• Formalized linear algebra over Elementary Divisor Rings in Coq
• A Mechanized Translation from Higher-Order Logic to Set Theory
• A formulation of the simple theory of types
• Elementary Divisors and Modules
• The elementary divisor theorem for certain rings without chain condition
• A Formal Proof of the Computation of Hermite Normal Form in a General Setting

This page was built for publication: A formalization of the Smith normal form in higher-order logic