Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
From MaRDI portal
Publication:333325
DOI10.1007/S00165-016-0383-1zbMATH Open1348.68213OpenAlexW2471798638MaRDI QIDQ333325FDOQ333325
Recommendations
- A Formal Proof of the Computation of Hermite Normal Form in a General Setting
- A formalization of the Smith normal form in higher-order logic
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Formalization and execution of linear algebra: from theorems to algorithms
- Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL
Cites work
- scientific article; zbMATH DE number 6013704 (Why is no real title available?)
- scientific article; zbMATH DE number 1531449 (Why is no real title available?)
- scientific article; zbMATH DE number 1534821 (Why is no real title available?)
- scientific article; zbMATH DE number 3445421 (Why is no real title available?)
- scientific article; zbMATH DE number 2116771 (Why is no real title available?)
- scientific article; zbMATH DE number 2123603 (Why is no real title available?)
- scientific article; zbMATH DE number 3401090 (Why is no real title available?)
- scientific article; zbMATH DE number 3109251 (Why is no real title available?)
- A first course in differential equations with modeling applications
- A formal proof of Sasaki-Murao algorithm
- A refinement-based approach to computational algebra in Coq
- Animating the formalised semantics of a Java-like language
- Commutative algebra in the Mizar system
- Computation of approximate polynomial GCDs and an extension
- Fast parallel matrix and GCD computations
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Formalization and execution of linear algebra: from theorems to algorithms
- Formalized linear algebra over elementary divisor rings in \textsc{Coq}
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Refinements for free!
- The HOL Light theory of Euclidean space
Cited in
(13)- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Formalized linear algebra over elementary divisor rings in \textsc{Coq}
- Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
- 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
- Formal analysis of the kinematic Jacobian in screw theory
- A formal proof of Sasaki-Murao algorithm
- Echelon Form
- Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL
- Formalization and execution of linear algebra: from theorems to algorithms
- A formalization of the Smith normal form in higher-order logic
- Formalization of functional variation in HOL Light
- A Formal Proof of the Computation of Hermite Normal Form in a General Setting
Describes a project that uses
Uses Software
This page was built for publication: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q333325)
