A formalization of the Smith normal form in higher-order logic
From MaRDI portal
Publication:2102950
Principal ideal rings (13F10) Canonical forms, reductions, classification (15A21) Matrices over special rings (quaternions, finite fields, etc.) (15B33) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)
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
Cites work
- A bijective proof of Muir's identity and the Cauchy-Binet formula
- A Formal Proof of the Computation of Hermite Normal Form in a General Setting
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- A formulation of the simple theory of types
- A generic and executable formalization of signature-based Gröbner basis algorithms
- A mechanized translation from higher-order logic to set theory
- A refinement-based approach to computational algebra in Coq
- A verified efficient implementation of the LLL basis reduction algorithm
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- Algorithms for Hermite and Smith Normal Matrices and Linear Diophantine Equations
- Application of the Smith Normal Form to the Structure of Lattice Rules
- Commutative algebra in the Mizar system
- Elementary Divisors and Modules
- Exploring the structure of an algebra text with locales
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
- Formalized linear algebra over elementary divisor rings in \textsc{Coq}
- Formalizing ring theory in PVS
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- From types to sets by local type definition in higher-order logic
- scientific article; zbMATH DE number 194428 (Why is no real title available?)
- scientific article; zbMATH DE number 1888461 (Why is no real title available?)
- scientific article; zbMATH DE number 3323944 (Why is no real title available?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Locales: a module system for mathematical theories
- Mining the Archive of Formal Proofs
- Smith normal form in combinatorics
- Some Remarks About Elementary Divisor Rings
- Some remarks on elementary divisor rings. II
- The elementary divisor theorem for certain rings without chain condition
- The HOL Light theory of Euclidean space
- Theorem Proving in Higher Order Logics
Cited in
(8)- Using abstract stobjs in ACL2 to compute matrix normal forms
- Correction to: ``A formalization of the Smith normal form in higher-order logic
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
- Formalization and execution of linear algebra: from theorems to algorithms
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Formalized linear algebra over elementary divisor rings in \textsc{Coq}
- Constructing the Lie algebra of smooth vector fields on a Lie group in Isabelle/HOL
- A Unified Framework for Formalizing Matrix Decomposition Proofs
Describes a project that uses
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)
