A Formalization of the Smith Normal Form in Higher-Order Logic

Referencias bibliográficas

• Adelsberger, S., Hetzl, S., Pollak, F.: The Cayley–Hamilton Theorem. Archive of Formal Proofs (2014) (formal proof development). http://afp.sf.net/entries/Cayley_Hamilton.shtml
• Aransay, J., Divasón, J.: Formalisation in higher-order logic and code generation to functional languages of the Gauss–Jordan algorithm. J. Funct. Program. (2015). https://doi.org/10.1017/S0956796815000155
• Aransay, J., Divasón, J.: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL. Form. Asp. Comput. 28(6), 1005–1026 (2016)
• Aransay, J., Divasón, J.: A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem. J. Autom. Reason. 58(4), 509–535 (2017)
• Archive of Formal Proofs. http://isa-afp.org/
• Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123–153 (2014)
• Ballarin, C.: Exploring the structure of an algebra text with locales. J. Autom. Reason. 64(6), 1093–1121 (2020)
• Bendich, P., Edelsbrunner, H., Kerber, M.: Computing robustness and persistence for images. IEEE Trans. Vis. Comput. Graph. 16(6), 1251–1260 (2010)
• Bottesch, R., Divasón, J., Thiemann, R.: Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation. Archive of Formal Proofs, March (2021) (formal proof development). https://isa-afp.org/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html
• Bottesch, R., Haslbeck, M.W., Thiemann, R.: A verified efficient implementation of the LLL basis reduction algorithm. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) Proceedings of 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPiC Series in Computing, vol. 57, pp. 164–180. EasyChair (2018)
• Bradley, G.H.: Algorithms for Hermite and Smith normal matrices and linear Diophantine equations. Math. Comput. 25(116), 897–907 (1971)
• Burton, D.: A First Course in Rings and Ideals. Addison-Wesley Series in Mathematics, Addison Wesley, Boston (1970)
• Cano, G., Cohen, C., Dénès, M., Mörtberg, A., Siles, V.: Formalized linear algebra over elementary divisor rings in Coq. Logical Methods in Computer Science (2016). https://doi.org/10.2168/LMCS-10.2168/LMCS-12(2:7)2016
• Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56–68 (1940)
• da Silva, A.B.A., de Lima, T.A., Galdino, A.L.: Formalizing ring theory in PVS. In: Avigad, J., Mahboubi, A. (eds.) Proceedings of the 9th International Conference on Interactive Theorem Proving, LNCS, vol. 10895, pp. 40–47. Springer (2018)
• Dénès, M., Mörtberg, A., Siles, V.: A refinement-based approach to computational algebra in Coq. In: Beringer, L., Felty, A.P. (eds.) Proceedings of the 3rd International Conference on Interactive Theorem Proving, LNCS, vol. 7406, pp. 83–98. Springer (2012)
• Divasón, J.: A verified algorithm for computing the Smith normal form of a matrix. Archive of Formal Proofs (May 2020) (formal proof development). http://isa-afp.org/entries/Smith_Normal_Form.html
• Divasón, J., Aransay, J.: Echelon form. Archive of Formal Proofs (2015) (formal proof development). http://afp.sf.net/entries/Echelon_Form.shtml
• Divasón, J., Aransay, J.: Hermite normal form. Archive of Formal Proofs, July (2015)
• Divasón, J., Aransay, J.: A formal proof of the computation of Hermite normal form in a general setting. In: Fleuriot, J.D., Wang, D., Calmet, J. (eds.) Proceedings of the 13th International Conference on Artificial Intelligence and Symbolic Computation, LNCS, vol. 11110, pp. 37–53. Springer (2018)
• Divasón, J., Aransay, J.: Towards a verified Smith normal form algorithm in Isabelle/HOL. In: Artal, E., Cogolludo, J. (eds.) Proceedings of the 16th EACA Zaragoza (Encuentros de Algebra Computacional y Aplicaciones), Monografías de la Real Academia de Ciencias, pp. 43–46 (2018)
• Divasón, J., Joosten, S., Kunčar, O., Thiemann, R., Yamada, A.: Efficient certification of complexity proofs: Formalizing the Perron–Frobenius theorem (invited talk paper). In: Andronick, J., Felty, A.P. (eds.) Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 2–13. ACM (2018)
• Divasón, J., Joosten, S.J.C., Thiemann, R., Yamada, A.: A verified implementation of the Berlekamp–Zassenhaus factorization algorithm. J. Autom. Reason. 64(4), 699–735 (2020)
• Dousson, X., Rubio, J., Sergeraert, F., Siret, Y.: The Kenzo Program. Institut Fourier, Grenoble (1999)
• Gamboa, R., Cowles, J., Baalen, J.V.: Using ACL2 arrays to formalise matrix algebra. In: 4th International Workshop on the ACL2 Theorem Prover and Its Applications (2003)
• Gillman, L., Henriksen, M.: Some remarks about elementary divisor rings. Trans. Am. Math. Soc. 82(2), 362–365 (1956)
• Haftmann, F.: Code generation from Isabelle/HOL theories (2021). https://isabelle.in.tum.de/doc/codegen.pdf
• Haftmann, F.: Haskell-style type classes with Isabelle/Isar (2021). https://isabelle.in.tum.de/doc/classes.pdf
• Harrison, J.: The HOL Light theory of Euclidean space. J. Autom. Reason. 50(2), 173–190 (2013)
• Helmer, O.: The elementary divisor theorem for certain rings without chain condition. Bull. Am. Math. Soc. 49(4), 225–236 (1943)
• Henriksen, M.: Some remarks on elementary divisor rings. II. Mich. Math. J. 3(2), 159–163 (1955)
• Howard, R.: Rings, Determinants, the Smith Normal Form, and Canonical Forms for Similarity of Matrices. Ralph Howard Department of Mathematics University of South Carolina, Columbia (2002)
• Huffman, B., Kuncar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) Proceedings of the 3rd ACM SIGPLAN International Conference on Certified Programs and Proofs, LNCS, vol. 8307, pp. 131–146. Springer (2013)
• Immler, F.: Example of use of local type definitions with linear algebra (2021). https://isabelle.in.tum.de/dist/library/HOL/HOL-Types_To_Sets/Linear_Algebra_On_With.html
• Immler, F., Zhan, B.: Smooth manifolds. Archive of Formal Proofs (October 2018) (formal proof development). http://isa-afp.org/entries/Smooth_Manifolds.html
• Isabelle Developers: HOL Analysis Library. Isabelle Developers (2021). https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/document.pdf
• Kaplansky, I.: Elementary divisors and modules. Trans. Am. Math. Soc. 66(2), 464–491 (1949)
• Krauss, A., Schropp, A.: A mechanized translation from higher-order logic to set theory. In: Kaufmann, M., Paulson, L.C. (eds.) Proceedings of the 1st International Conference on Interactive Theorem Proving, LNCS, vol. 6172, pp. 323–338. Springer (2010)
• Kunčar, O., Popescu, A.: From types to sets by local type definition in higher-order logic. J. Autom. Reason. 62(2), 237–260 (2019)
• Lawson, T.: Does Smith normal form imply PID? (2010). https://mathoverflow.net/questions/31275/does-smith-normal-form-imply-pid
• Lyness, J., Keast, P.: Application of the Smith normal form to the structure of lattice rules. SIAM J. Matrix Anal. Appl. 16(1), 218–231 (1995)
• Maciejowski, J.: Multivariable Feedback Design. Electronic Systems Engineering Series, Addison-Wesley, Boston (1989)
• Maletzky, A.: A generic and executable formalization of signature-based Gröbner basis algorithms. J. Symb. Comput. 106, 23–47 (2021)
• Narkawicz, A., Muñoz, 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)
• Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, LNCS vol. 2283. Springer (2002)
• Obua, S.: Proving bounds for real linear programs in Isabelle/HOL. In: Hurd, J., Melham, T.F. (eds.) Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics, LNCS, vol. 3603, pp. 227–244. Springer (2005)
• Rudnicki, P., Schwarzweller, C., Trybulec, A.: Commutative algebra in the Mizar system. J. Symb. Comput. 32(1/2), 143–169 (2001)
• Snášel, V., Nowaková, J., Xhafa, F., Barolli, L.: Geometrical and topological approaches to big data. Future Gener. Comput. Syst. 67, 286–296 (2017)
• StackExchange Mathematics. Problem with Smith normal form over a PID that is not a Euclidean domain (2014). https://bit.ly/2rWLqxG
• Stanley, R.P.: Smith normal form in combinatorics. J. Comb. Theory A 144, 476–495 (2016)
• Storjohann, A.: Algorithms for matrix canonical forms. PhD Thesis, Swiss Federal Institute of Technology Zurich (2000)
• Strang, G.: Introduction to Linear Algebra. Wellesley-Cambridge Press, Wellesley (2009)
• Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle/HOL. In: Proceedings of the 5th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 88–99. ACM (2016)
• Zeng, J.: A bijective proof of Muir’s identity and the Cauchy–Binet formula. Linear Algebra Appl. 184, 79–82 (1993)