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


BibTeX

@inproceedings{LM-TACAS20,
author = "Alexander Lochmann and Aart Middeldorp",
title = "Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting",
booktitle = "Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems",
editor = "Armin Biere and Dave Parker",
series = "Lecture Notes in Computer Science",
volume = 12079,
pages = "178--194",
year = 2020,
doi = "10.1007/978-3-030-45237-7_11"
}


Nach oben scrollen