A Formal Proof of the Computation of Hermite Normal Form in a General Setting
From MaRDI portal
Publication:6108811
DOI10.1007/978-3-319-99957-9_3zbMath1515.68350MaRDI QIDQ6108811
Publication date: 30 June 2023
Published in: Artificial Intelligence and Symbolic Computation (Search for Journal in Brave)
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)
Related Items
A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem, A formalization of the Smith normal form in higher-order logic
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
- 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
- A decision algorithm for linear sentences on a PFM
- An application of the Hermite normal form in integer programming
- Isabelle/HOL. A proof assistant for higher-order logic
- Using abstract stobjs in ACL2 to compute matrix normal forms
- Beyond unimodular transformations
- The HOL Light theory of Euclidean space
- 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
- Flyspeck II: The basic linear programs
- The Misfortunes of a Trio of Mathematicians Using Computer Algebra Systems. Can We Trust in Them?
- From Types to Sets by Local Type Definitions in Higher-Order Logic
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Refinements for Free!
- A Rigorous Subexponential Algorithm For Computation of Class Groups
- Verifying a Compiler for Java Threads
- Fast Parallel Computation of Hermite and Smith Forms of Polynomial Matrices
- Polynomial Algorithms for Computing the Smith and Hermite Normal Forms of an Integer Matrix
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Algorithms for Hermite and Smith Normal Matrices and Linear Diophantine Equations
- Formalized linear algebra over Elementary Divisor Rings in Coq
