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

The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattic...

Descripción completa

Detalles Bibliográficos
Autores principales: Thiemann, René, Bottesch, Ralph, Divasón, Jose, Haslbeck, Max W., Joosten, Sebastiaan J. C., Yamada, Akihisa
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Springer Netherlands 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7413592/
https://www.ncbi.nlm.nih.gov/pubmed/32831440
http://dx.doi.org/10.1007/s10817-020-09552-1

Internet

https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7413592/
https://www.ncbi.nlm.nih.gov/pubmed/32831440
http://dx.doi.org/10.1007/s10817-020-09552-1

Ejemplares similares