A formalization of the Smith normal form in higher-order logic
From MaRDI portal
Publication:2102950
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)
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
- 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?)
- A Formal Proof of the Computation of Hermite Normal Form in a General Setting
- A bijective proof of Muir's identity and the Cauchy-Binet formula
- 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
- 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 HOL Light theory of Euclidean space
- The elementary divisor theorem for certain rings without chain condition
- Theorem Proving in Higher Order Logics
Cited in
(6)- Formalized linear algebra over elementary divisor rings in \textsc{Coq}
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Using abstract stobjs in ACL2 to compute matrix normal forms
- Formalization and execution of linear algebra: from theorems to algorithms
- Correction to: ``A formalization of the Smith normal form in higher-order logic
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)
