Using abstract stobjs in ACL2 to compute matrix normal forms

DOI10.1007/978-3-319-66107-0_23zbMATH Open1484.68312OpenAlexW2750465938MaRDI QIDQ1687754FDOQ1687754

Authors: Laureano Lambán, Francisco Jesús Martín-Mateos, Julio Rubio, José Luis Ruiz-Reina 

Publication date: 4 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-66107-0_23

Recommendations

• Computing with abstract matrix structures
• Logic Based Program Synthesis and Transformation
• A formalization of the Smith normal form in higher-order logic
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Abstract matrices in symbolic computation

zbMATH Keywords

matricesACL2matrix normal formsabstract stobjs

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Data structures (68P05) Matrices of integers (15B36) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Hermite Normal Form Computation Using Modulo Determinant Arithmetic
• Point-free, set-free concrete linear algebra
• Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
• Formalized linear algebra over elementary divisor rings in \textsc{Coq}
• The Smith normal form
• Computing persistent homology within Coq/SSReflect

Cited In (1)

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

Uses Software

• ACL2
• Coq/SSReflect

This page was built for publication: Using abstract stobjs in ACL2 to compute matrix normal forms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1687754)