Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL

René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, Akihisa Yamada 0002. Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL. Journal of Automated Reasoning, 64(5):827-856, 2020. [doi]

Abstract

Abstract is missing.