A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
From MaRDI portal
Publication:2362109
DOI10.1007/s10817-016-9379-zzbMath1409.68249OpenAlexW2420264810MaRDI QIDQ2362109
Publication date: 6 July 2017
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-016-9379-z
symbolic computationleast squares problemlinear algebracode generationinteractive theorem proving\( QR \) decomposition
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Formalization and Execution of Linear Algebra: From Theorems to Algorithms ⋮ On the formalization of Gram-Schmidt process for orthonormalizing a set of vectors ⋮ 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
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Proving tight bounds on univariate expressions with elementary functions in Coq
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
- Isabelle/HOL. A proof assistant for higher-order logic
- The HOL Light theory of Euclidean space
- Verified compilation of floating-point computations
- 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
- Algebraic Numbers in Isabelle/HOL
- A compiled implementation of normalisation by evaluation
- A Refinement-Based Approach to Computational Algebra in Coq
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Refinements for Free!
- Formalization of real analysis: a survey of proof assistants and libraries
- Point-Free, Set-Free Concrete Linear Algebra
- Mining the Archive of Formal Proofs
- Formalization and Execution of Linear Algebra: From Theorems to Algorithms
- Numerical Methods in Scientific Computing, Volume I
- Real Number Calculations and Theorem Proving
- Code Generation via Higher-Order Rewrite Systems
- Constructive Type Classes in Isabelle
- The Fundamental Theorem of Linear Algebra
- Verified Real Number Calculations: A Library for Interval Arithmetic
- Efficient Formal Verification of Bounds of Linear Programs
- A FORMAL PROOF OF THE KEPLER CONJECTURE
- Automatic Data Refinement
- Data Refinement in Isabelle/HOL
- A Machine-Checked Proof of the Odd Order Theorem
- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
- Theorem Proving in Higher Order Logics
- Formalization of Complex Vectors in Higher-Order Logic
- A Formal Proof of the Computation of Hermite Normal Form in a General Setting
This page was built for publication: A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
