Reseña: A formal proof of the computation of Hermite normal form in a general setting

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado REGULAR-MT: A formal proof of the computation of Hermite normal form in a general setting.

Sus autores son Jose Divasón y Jesús Aransay (de la Universidad de la Rioja).

Su resumen es

In this work, we present a formal proof of an algorithm to compute the Hermite normal form of a matrix based on our existing framework for the formalisation, execution, and refinement of linear algebra algorithms in Isabelle/HOL. The Hermite normal form is a well-known canonical matrix analogue of reduced echelon form of matrices over fields, but involving matrices over more general rings, such as Bézout domains. We prove the correctness of this algorithm and formalise the uniqueness of the Hermite normal form of a matrix. The succinctness and clarity of the formalisation validate the usability of the framework.

El trabajo se presentará el 17 de septiembre en el AISC 2018 (13th International Conference on Artificial Intelligence and Symbolic Computation).

El código de las correspondientes teorías se encuentra aquí.