Divasón, Jose; Thiemann, René A formalization of the Smith normal form in higher-order logic. (English) Zbl 1511.68309 J. Autom. Reasoning 66, No. 4, 1065-1095 (2022); correction ibid. 66, No. 4, 1097 (2022). Reviewer: Filippo Nuccio (Saint-Étienne) MSC: 68V15 13F10 15A21 15B33 68V20 PDFBibTeX XMLCite \textit{J. Divasón} and \textit{R. Thiemann}, J. Autom. Reasoning 66, No. 4, 1065--1095 (2022; Zbl 1511.68309) Full Text: DOI
Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. (English) Zbl 1469.68165 J. Autom. Reasoning 64, No. 4, 699-735 (2020). MSC: 68V15 03B35 12-08 13P05 68V20 PDFBibTeX XMLCite \textit{J. Divasón} et al., J. Autom. Reasoning 64, No. 4, 699--735 (2020; Zbl 1469.68165) Full Text: DOI
Divasón, Jose; Aransay, Jesús A formal proof of the computation of Hermite normal form in a general setting. (English) Zbl 1515.68350 Fleuriot, Jacques (ed.) et al., Artificial intelligence and symbolic computation. 13th international conference, AISC 2018, Suzhou, China, September 16–19, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11110, 37-53 (2018). MSC: 68V20 15A21 68V15 PDFBibTeX XMLCite \textit{J. Divasón} and \textit{J. Aransay}, Lect. Notes Comput. Sci. 11110, 37--53 (2018; Zbl 1515.68350) Full Text: DOI