Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
From MaRDI portal
Publication:333325
DOI10.1007/s00165-016-0383-1zbMath1348.68213OpenAlexW2471798638MaRDI QIDQ333325
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
Symbolic computation and algebraic computation (68W30) Canonical forms, reductions, classification (15A21)
Related Items
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 and Execution of Linear Algebra: From Theorems to Algorithms, Using abstract stobjs in ACL2 to compute matrix normal forms, A Formal Proof of the Computation of Hermite Normal Form in a General Setting, Formalization of functional variation in HOL Light, Echelon Form, A formalization of the Smith normal form in higher-order logic
Uses Software
Cites Work
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- Commutative algebra in the Mizar system
- Computation of approximate polynomial GCDs and an extension
- The HOL Light theory of Euclidean space
- A Refinement-Based Approach to Computational Algebra in Coq
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Refinements for Free!
- Animating the Formalised Semantics of a Java-Like Language
- Formalization and Execution of Linear Algebra: From Theorems to Algorithms
- Fast parallel matrix and GCD computations
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Formalized linear algebra over Elementary Divisor Rings in Coq
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
