Formalization and Execution of Linear Algebra: From Theorems to Algorithms

DOI10.1007/978-3-319-14125-1_1zbMath1453.68210OpenAlexW613166357WikidataQ57721911 ScholiaQ57721911MaRDI QIDQ3453644

Jesús Aransay, Jose Divasón

Publication date: 30 November 2015

Published in: Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-14125-1_1

zbMATH Keywords

verificationlinear algebracode generation

Mathematics Subject Classification ID

Biomedical imaging and signal processing (92C55) Linear transformations, semilinear transformations (15A04) Direct numerical methods for linear systems and matrix inversion (65F05) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (6)

A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL ⋮ Unnamed Item ⋮ Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm ⋮ Modelling algebraic structures and morphisms in ACL2

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• Coq/SSReflect
• Autoref
• Gauss-Jordan
• Gauss Jordan Elimination
• Rank Nullity

Cites Work

• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• A revision of the proof of the Kepler conjecture
• Formalizing Arrow's theorem
• Isabelle/HOL. A proof assistant for higher-order logic
• The HOL Light theory of Euclidean space
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• Towards a Certified Computation of Homology Groups for Digital Images
• A Refinement-Based Approach to Computational Algebra in Coq
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Computing persistent homology within Coq/SSReflect
• Code Generation via Higher-Order Rewrite Systems
• Incidence Simplicial Matrices Formalized in Coq/SSReflect
• Automatic Data Refinement
• Data Refinement in Isabelle/HOL
• Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• Theorem Proving in Higher Order Logics
• Unnamed Item

This page was built for publication: Formalization and Execution of Linear Algebra: From Theorems to Algorithms