Generalizing a Mathematical Analysis Library in Isabelle/HOL

详细信息    查看全文

• 作者：Jes煤s Aransay (16)
  Jose Divas贸n (16)
  
  16. Departamento de Matem谩ticas y Computaci贸n ; Universidad de La Rioja ; Logro帽o ; Spain
  
• 关键词：Theorem proving ; Isabelle/HOL ; Type classes ; Linear Algebra
• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：9058
• 期：1
• 页码：415-421
• 全文大小：144 KB
• 参考文献：1. Harrison, J (2013) The HOL Light Theory of Euclidean Space. J. Autom. Reasoning. 50: pp. 173-190 9250-9" target="_blank" title="It opens in new window">CrossRef
  2. Heras, J, D茅n猫s, M, Mata, G, M枚rtberg, A, Poza, M, Siles, V Towards a certified computation of homology groups for digital images. In: Ferri, M, Frosini, P, Landi, C, Cerri, A, Fabio, B eds. (2012) Computational Topology in Image Context. Springer, Heidelberg, pp. 49-57 978-3-642-30238-1_6" target="_blank" title="It opens in new window">CrossRef
  3. Avigad, J., H枚lzl, J., Serafin, L.: A formally verified proof of the Central Limit Theorem. CoRR (2014)
  4. H枚lzl, J, Immler, F, Huffman, B Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S, Paulin-Mohring, C, Pichardie, D eds. (2013) Interactive Theorem Proving. Springer, Heidelberg, pp. 279-294 978-3-642-39634-2_21" target="_blank" title="It opens in new window">CrossRef
  5. http://www.unirioja.es/cu/jodivaso/Isabelle/Gauss-Jordan-2013-2/
  6. Axler, S.: Linear Algebra Done Right, 2nd edn. Springer (2004)
  7. Strang, G.: Introduction to Linear Algebra. Wellesley - Cambridge Press (2009)
  8. Aransay, J., Divas贸n, J.: Rank-Nullity Theorem in Linear Algebra. AFP (2013)
  9. Mackiw, G (1995) A Note on the Equality of the Column and Row Rank of a Matrix. Mathematics Magazine 68: pp. 285-286 90576" target="_blank" title="It opens in new window">CrossRef
  10. Aransay, J., Divas贸n, J.: Gauss-Jordan Algorithm and its Applications. AFP (2014)
  11. http://www.math4all.in/public_html/linearalgebra/chapter3.4.html
  12. Dur谩n, AJ, P茅rez, M, Varona, JL (2014) The Misfortunes of a Trio of Mathematicians Using Computer Algebra Systems. Can We Trust in Them?. Notices of the AMS 51: pp. 1249-1252 90/noti1173" target="_blank" title="It opens in new window">CrossRef
  
• 作者单位：NASA Formal Methods
• 丛书名：978-3-319-17523-2
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

The HOL Multivariate Analysis Library (HMA) of Isabelle/HOL is focused on concrete types such as \(\mathbb {R}\) , \(\mathbb {C}\) and \(\mathbb {R}^n\) and on algebraic structures such as real vector spaces and Euclidean spaces, represented by means of type classes. The generalization of HMA to more abstract algebraic structures is something desirable but it has not been tackled yet. Using that library, we were able to prove the Gauss-Jordan algorithm over real matrices, but our interest lied on generating verified code for matrices over arbitrary fields, greatly increasing the range of applications of such an algorithm. This short paper presents the steps that we did and the methodology that we devised to generalize such a library, which were successful to generalize the Gauss-Jordan algorithm to matrices over arbitrary fields.