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
Authors: Jesús Aransay, Jose Divasón 
Publication date: 28 October 2016
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-016-0383-1
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
Symbolic computation and algebraic computation (68W30) Canonical forms, reductions, classification (15A21)
Cites Work
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Computation of approximate polynomial GCDs and an extension
- Title not available (Why is that?)
- 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
- Formalization and execution of linear algebra: from theorems to algorithms
- Title not available (Why is that?)
- Commutative algebra in the Mizar system
- The HOL Light theory of Euclidean space
- Refinements for free!
- Animating the formalised semantics of a Java-like language
- Title not available (Why is that?)
- Title not available (Why is that?)
- Fast parallel matrix and GCD computations
- Title not available (Why is that?)
- A formal proof of Sasaki-Murao algorithm
- 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}
- A first course in differential equations with modeling applications
Cited In (13)
- A formalization of the Smith normal form in higher-order logic
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Formal analysis of the kinematic Jacobian in screw theory
- Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL
- Formalization of functional variation in HOL Light
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Echelon Form
- Formalization and execution of linear algebra: from theorems to algorithms
- Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
- Using abstract stobjs in ACL2 to compute matrix normal forms
- A Formal Proof of the Computation of Hermite Normal Form in a General Setting
- Formalized linear algebra over elementary divisor rings in \textsc{Coq}
- A formal proof of Sasaki-Murao algorithm
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)
