Using abstract stobjs in ACL2 to compute matrix normal forms

DOI10.1007/978-3-319-66107-0_23MaRDI QIDQ1687754zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(1)

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

Describes a project that uses

Uses Software

• Coq/SSReflect
• ACL2

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)