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

From MaRDI portal
Set OpenAlex properties.
ReferenceBot (talk | contribs)
Changed an Item
Property / cites work
 
Property / cites work: A compiled implementation of normalisation by evaluation / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formalization of Complex Vectors in Higher-Order Logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formalization and Execution of Linear Algebra: From Theorems to Algorithms / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4868585 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Mining the Archive of Formal Proofs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Verified compilation of floating-point computations / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formalization of real analysis: a survey of proof assistants and libraries / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3497626 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Refinements for Free! / rank
 
Normal rank
Property / cites work
 
Property / cites work: Numerical Methods in Scientific Computing, Volume I / rank
 
Normal rank
Property / cites work
 
Property / cites work: Verified Real Number Calculations: A Library for Interval Arithmetic / rank
 
Normal rank
Property / cites work
 
Property / cites work: A Refinement-Based Approach to Computational Algebra in Coq / rank
 
Normal rank
Property / cites work
 
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 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A Formal Proof of the Computation of Hermite Normal Form in a General Setting / rank
 
Normal rank
Property / cites work
 
Property / cites work: Point-Free, Set-Free Concrete Linear Algebra / rank
 
Normal rank
Property / cites work
 
Property / cites work: A Machine-Checked Proof of the Odd Order Theorem / rank
 
Normal rank
Property / cites work
 
Property / cites work: Data Refinement in Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank
 
Normal rank
Property / cites work
 
Property / cites work: Constructive Type Classes in Isabelle / rank
 
Normal rank
Property / cites work
 
Property / cites work: A FORMAL PROOF OF THE KEPLER CONJECTURE / rank
 
Normal rank
Property / cites work
 
Property / cites work: Theorem Proving in Higher Order Logics / rank
 
Normal rank
Property / cites work
 
Property / cites work: The HOL Light theory of Euclidean space / rank
 
Normal rank
Property / cites work
 
Property / cites work: Type Classes and Filters for Mathematical Analysis in Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: Automatic Data Refinement / rank
 
Normal rank
Property / cites work
 
Property / cites work: Real Number Calculations and Theorem Proving / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proving tight bounds on univariate expressions with elementary functions in Coq / rank
 
Normal rank
Property / cites work
 
Property / cites work: Isabelle/HOL. A proof assistant for higher-order logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Flyspeck II: The basic linear programs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Efficient Formal Verification of Bounds of Linear Programs / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Fundamental Theorem of Linear Algebra / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4799718 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Algebraic Numbers in Isabelle/HOL / rank
 
Normal rank

Revision as of 01:52, 14 July 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

    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
    6 July 2017
    0 references
    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
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers