A formalization of the Smith normal form in higher-order logic
DOI10.1007/S10817-022-09631-5OpenAlexW4281558819MaRDI QIDQ2102950FDOQ2102950
Authors: 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
Recommendations
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
- A Formal Proof of the Computation of Hermite Normal Form in a General Setting
- Formalized linear algebra over elementary divisor rings in \textsc{Coq}
- scientific article; zbMATH DE number 1118055
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
Matrices over special rings (quaternions, finite fields, etc.) (15B33) Canonical forms, reductions, classification (15A21) Formalization of mathematics in connection with theorem provers (68V20) Principal ideal rings (13F10) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
- Mining the Archive of Formal Proofs
- Isabelle/HOL. A proof assistant for higher-order logic
- Application of the Smith Normal Form to the Structure of Lattice Rules
- A formulation of the simple theory of types
- Locales: a module system for mathematical theories
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- A refinement-based approach to computational algebra in Coq
- Title not available (Why is that?)
- A mechanized translation from higher-order logic to set theory
- Commutative algebra in the Mizar system
- Smith normal form in combinatorics
- The HOL Light theory of Euclidean space
- Some Remarks About Elementary Divisor Rings
- Elementary Divisors and Modules
- The elementary divisor theorem for certain rings without chain condition
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Formalized linear algebra over Elementary Divisor Rings in Coq
- Title not available (Why is that?)
- Some remarks on elementary divisor rings. II
- Theorem Proving in Higher Order Logics
- Algorithms for Hermite and Smith Normal Matrices and Linear Diophantine Equations
- Title not available (Why is that?)
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- From types to sets by local type definition in higher-order logic
- Formalizing ring theory in PVS
- A bijective proof of Muir's identity and the Cauchy-Binet formula
- A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
- A generic and executable formalization of signature-based Gröbner basis algorithms
- Exploring the structure of an algebra text with locales
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- A Formal Proof of the Computation of Hermite Normal Form in a General Setting
Cited In (1)
Uses Software
This page was built for publication: A formalization of the Smith normal form in higher-order logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2102950)
