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
Changed an Item
Created claim: Wikidata QID (P12): Q57721904, #quickstatements; #temporary_batch_1729946815562
(17 intermediate revisions by 4 users not shown)
Property / describes a project that uses
 
Property / describes a project that uses: Rank Nullity / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Real_Impl / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: GitHub / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Isabelle / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Mathematica / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Archive Formal Proofs / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Autoref / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: HOL / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Isabelle/HOL / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: PVS / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Flyspeck / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Cayley-Hamilton / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Echelon Form / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Gauss-Jordan / rank
 
Normal rank
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / full work available at URL
 
Property / full work available at URL: https://doi.org/10.1007/s10817-016-9379-z / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W2420264810 / rank
 
Normal rank
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
Property / Wikidata QID
 
Property / Wikidata QID: Q57721904 / rank
 
Normal rank

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

    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