A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (Q2362109): Difference between revisions

Revision as of 13:58, 26 October 2024

scientific article

Language	Label	Description	Also known as
English	A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem	scientific article

Statements

instance of

scholarly article

0 references

title

A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (English)

0 references

0 references

0 references

Journal of Automated Reasoning

0 references

publication date

6 July 2017

0 references

zbMATH Keywords

least squares problem

0 references

\( QR \) decomposition

0 references

interactive theorem proving

0 references

linear algebra

0 references

code generation

0 references

symbolic computation

0 references

describes a project that uses

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

Archive Formal Proofs

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

MaRDI publication profile

0 references

full work available at URL

https://doi.org/10.1007/s10817-016-9379-z

0 references

cites work

A compiled implementation of normalisation by evaluation

0 references

Formalization of Complex Vectors in Higher-Order Logic

0 references

Formalization and Execution of Linear Algebra: From Theorems to Algorithms

0 references

Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL

0 references

Q4868585

0 references

Mining the Archive of Formal Proofs

0 references

Verified compilation of floating-point computations

0 references

Formalization of real analysis: a survey of proof assistants and libraries

0 references

Q3497626

0 references

Refinements for Free!

0 references

Numerical Methods in Scientific Computing, Volume I

0 references

Verified Real Number Calculations: A Library for Interval Arithmetic

0 references

A Refinement-Based Approach to Computational Algebra in Coq

0 references

A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem

0 references

A Formal Proof of the Computation of Hermite Normal Form in a General Setting

0 references

Point-Free, Set-Free Concrete Linear Algebra

0 references

A Machine-Checked Proof of the Odd Order Theorem

0 references

Data Refinement in Isabelle/HOL

0 references

Code Generation via Higher-Order Rewrite Systems

0 references

Constructive Type Classes in Isabelle

0 references

A FORMAL PROOF OF THE KEPLER CONJECTURE

0 references

Theorem Proving in Higher Order Logics

0 references

The HOL Light theory of Euclidean space

0 references

Type Classes and Filters for Mathematical Analysis in Isabelle/HOL

0 references

Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL

0 references

Automatic Data Refinement

0 references

Real Number Calculations and Theorem Proving

0 references

Proving tight bounds on univariate expressions with elementary functions in Coq

0 references

Isabelle/HOL. A proof assistant for higher-order logic

0 references

Flyspeck II: The basic linear programs

0 references

Efficient Formal Verification of Bounds of Linear Programs

0 references

The Fundamental Theorem of Linear Algebra

0 references

Q4799718

0 references

Algebraic Numbers in Isabelle/HOL

0 references

Identifiers

zbMATH Open document ID

1409.68249

0 references

DOI

10.1007/s10817-016-9379-z

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

0 references

0 references

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:2362109

@@ Property / describes a project that uses @@
+Real_Impl
@@ Property / describes a project that uses: Real_Impl / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+GitHub
@@ Property / describes a project that uses: GitHub / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Mathematica
@@ Property / describes a project that uses: Mathematica / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Autoref
@@ Property / describes a project that uses: Autoref / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PVS
@@ Property / describes a project that uses: PVS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Flyspeck
@@ Property / describes a project that uses: Flyspeck / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Cayley-Hamilton
@@ Property / describes a project that uses: Cayley-Hamilton / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Echelon Form
@@ Property / describes a project that uses: Echelon Form / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Gauss-Jordan
@@ Property / describes a project that uses: Gauss-Jordan / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-016-9379-z
+Normal rank
@@ Property / OpenAlex ID @@
+W2420264810
@@ Property / OpenAlex ID: W2420264810 / rank @@
+Normal rank
@@ Property / cites work @@
+A compiled implementation of normalisation by evaluation
+Normal rank
@@ Property / cites work @@
+Formalization of Complex Vectors in Higher-Order Logic
+Normal rank
@@ Property / cites work @@
+Formalization and Execution of Linear Algebra: From Theorems to Algorithms
+Normal rank
@@ Property / cites work @@
+Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Q4868585
@@ Property / cites work: Q4868585 / rank @@
+Normal rank
@@ Property / cites work @@
+Mining the Archive of Formal Proofs
@@ Property / cites work: Mining the Archive of Formal Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Verified compilation of floating-point computations
+Normal rank
@@ Property / cites work @@
+Formalization of real analysis: a survey of proof assistants and libraries
+Normal rank
@@ Property / cites work @@
+Q3497626
@@ Property / cites work: Q3497626 / rank @@
+Normal rank
@@ Property / cites work @@
+Refinements for Free!
@@ Property / cites work: Refinements for Free! / rank @@
+Normal rank
@@ Property / cites work @@
+Numerical Methods in Scientific Computing, Volume I
+Normal rank
@@ Property / cites work @@
+Verified Real Number Calculations: A Library for Interval Arithmetic
+Normal rank
@@ Property / cites work @@
+A Refinement-Based Approach to Computational Algebra in Coq
+Normal rank
@@ Property / cites work @@
+A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
+Normal rank
@@ Property / cites work @@
+A Formal Proof of the Computation of Hermite Normal Form in a General Setting
+Normal rank
@@ Property / cites work @@
+Point-Free, Set-Free Concrete Linear Algebra
@@ Property / cites work: Point-Free, Set-Free Concrete Linear Algebra / rank @@
+Normal rank
@@ Property / cites work @@
+A Machine-Checked Proof of the Odd Order Theorem
@@ Property / cites work: A Machine-Checked Proof of the Odd Order Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+Data Refinement in Isabelle/HOL
@@ Property / cites work: Data Refinement in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Code Generation via Higher-Order Rewrite Systems
@@ Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive Type Classes in Isabelle
@@ Property / cites work: Constructive Type Classes in Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+A FORMAL PROOF OF THE KEPLER CONJECTURE
@@ Property / cites work: A FORMAL PROOF OF THE KEPLER CONJECTURE / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+The HOL Light theory of Euclidean space
@@ Property / cites work: The HOL Light theory of Euclidean space / rank @@
+Normal rank
@@ Property / cites work @@
+Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Automatic Data Refinement
@@ Property / cites work: Automatic Data Refinement / rank @@
+Normal rank
@@ Property / cites work @@
+Real Number Calculations and Theorem Proving
@@ Property / cites work: Real Number Calculations and Theorem Proving / rank @@
+Normal rank
@@ Property / cites work @@
+Proving tight bounds on univariate expressions with elementary functions in Coq
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Flyspeck II: The basic linear programs
@@ Property / cites work: Flyspeck II: The basic linear programs / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient Formal Verification of Bounds of Linear Programs
+Normal rank
@@ Property / cites work @@
+The Fundamental Theorem of Linear Algebra
@@ Property / cites work: The Fundamental Theorem of Linear Algebra / rank @@
+Normal rank
@@ Property / cites work @@
+Q4799718
@@ Property / cites work: Q4799718 / rank @@
+Normal rank
@@ Property / cites work @@
+Algebraic Numbers in Isabelle/HOL
@@ Property / cites work: Algebraic Numbers in Isabelle/HOL / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q57721904
@@ Property / Wikidata QID: Q57721904 / rank @@
+Normal rank