Using abstract stobjs in ACL2 to compute matrix normal forms

DOI10.1007/978-3-319-66107-0_23zbMath1484.68312OpenAlexW2750465938MaRDI QIDQ1687754

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

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)

Related Items (1)

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

Uses Software

• ACL2
• Coq/SSReflect

Cites Work

• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• The Smith normal form
• Computing persistent homology within Coq/SSReflect
• 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 Coq

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