Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Automated Reasoning in the Age of the Internet Read chapter Read first chapter

2018 | OriginalPaper | Chapter

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

Authors : Jose Divasón, Jesús Aransay

Published in: Artificial Intelligence and Symbolic Computation

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Methodologies of Symbolic Computation
next chapter Formalizing Some “Small” Finite Models of Projective Geometry in Coq
Footnotes
1
The Isabelle file that serialises https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-99957-9_3/MediaObjects/473073_1_En_3_Figaa_HTML.gif to UArrays is available from our website [16].
 
2
Neither records nor locales [9] are used for this task, although they are a valid alternative.
 
Literature
1.
2.
3.
4.
5.
6.
7.
8.
Aransay, J., Divasón, J.: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL. Formal Aspects Comput. 28(6), 1005–1026 (2016)MathSciNetCrossRef
9.
10.
Bradley, G.H.: Algorithms for Hermite and Smith normal matrices and linear diophantine equations. Math. Comput. 25(116), 897–907 (1971)MathSciNetCrossRef
11.
Cano, G., Cohen, C., Dénès, M., Mörtberg, A., Siles, V.: Formalized linear algebra over elementary divisor rings in Coq. Logical Methods Comput. Sci. 12(2) (2016)
12.
13.
14.
Coquand, T., Mörtberg, A., Siles, V.: A formal proof of Sasaki-Murao algorithm. J. Formalized Reason. 5(1), 27–36 (2012)MathSciNet
15.
16.
17.
Divasón, J., Aransay, J.: Hermite normal form. Archive of Formal Proofs, July 2015
18.
Durán, A.J., Pérez, M., Varona, J.L.: The Misfortunes of a trio of mathematicians using computer algebra systems. Can we trust in them? Not. AMS 61(10), 1249–1252 (2014)
19.
Gamboa, R., Cowles, J., Baalen, J.V.: Using ACL2 arrays to formalise matrix algebra. In: Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (2003)
20.
21.
Hafner, J.L., McCurley, K.S.: A rigorous subexponential algorithm for computation of class groups. J. Am. Math. Soc. 2(4), 837–850 (1989)MathSciNetCrossRef
22.
23.
24.
25.
Hung, M.S., Rom, W.O.: An application of the Hermite normal form in integer programming. Linear Algebra Appl. 140, 163–179 (1990)MathSciNetCrossRef
26.
Kaltofen, E., Krishnamoorthy, M.S., Saunders, B.D.: Fast parallel computation of Hermite and Smith forms of polynomial matrices. SIAM J. Algebraic Discrete Methods 8(4), 683–690 (1987)MathSciNetCrossRef
27.
Kannan, R., Bachem, A.: Polynomial algorithms for computing the Smith and Hermite normal forms of an integer matrix. SIAM J. Comput. 8(4), 499–507 (1979)MathSciNetCrossRef
28.
Klein , G., et al.: seL4: formal verification of an OS kernel. In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles, SOSP 2009, Big Sky, Montana, USA, pp. 207–220 (2009)
29.
Kunčar, O., Popescu, A.: From types to sets by local type definitions in higher-order logic. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving. pp, pp. 200–218. Springer International Publishing, Cham (2016)CrossRef
30.
31.
Li, L., Li, H., Liu, Y.: A decision algorithm for linear sentences on a PFM. Ann. Pure Appl. Logic 59, 273–286 (1993)MathSciNetCrossRef
32.
Li, W., Paulson, L.C.: A modular, efficient formalisation of real algebraic numbers. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, 20–22 January 2016, pp. 66–75 (2016)
33.
34.
Narkawicz, A., Muoz, C., Dutle, A.: Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems. J. Autom. Reason. 54(4), 285–326 (2015)MathSciNetCrossRef
35.
Newman, M.: Integral Matrices. Pure and Applied Mathematics. Elsevier Science, New York (1972)
36.
37.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic (2018). Updated version of the book with the same title and authors
38.
Obua, S., Nipkow, T.: Flyspeck II: the basic linear programs. Ann. Math. Artif. Intell. 56(3–4), 245–272 (2009)MathSciNetCrossRef
39.
Paulson, L.C.: A mechanised proof of Gödel’s incompleteness theorems using nominal Isabelle. J. Autom. Reason. 55(1), 1–37 (2015)CrossRef
40.
Ramanujam, J.: Beyond unimodular transformations. J. Supercomput. 9(4), 365–389 (1995)CrossRef
41.
Rudnicki, P., Schwarzweller, C., Trybulec, A.: Commutative algebra in the Mizar system. J. Symbolic Comput. 32(1/2), 143–169 (2001)MathSciNetCrossRef
42.
Sternagel, C., Thiemann, R.: Executable matrix operations on matrices of arbitrary dimensions. Archive of Formal Proofs, June 2010
43.
Storjohann, A.: Algorithms for matrix canonical forms. Ph.D. thesis, Swiss Federal Institute of Technology, Zurich (2000)
44.
Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle/HOL. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, 20–22 January 2016, pp. 88–99 (2016)
45.
Tourloupis, V.E.: Hermite normal forms and its cryptographic applications. Master’s thesis, University of Wollongong (2013)
Metadata
Title
A Formal Proof of the Computation of Hermite Normal Form in a General Setting
Authors
Jose Divasón
Jesús Aransay
Copyright Year
2018
Book
Artificial Intelligence and Symbolic Computation

Print ISBN: 978-3-319-99956-2

Electronic ISBN: 978-3-319-99957-9

Copyright Year: 2018

DOI
https://doi.org/10.1007/978-3-319-99957-9_3

Premium Partner

    Image Credits