diff --git a/metadata/entries/Berlekamp_Zassenhaus.toml b/metadata/entries/Berlekamp_Zassenhaus.toml --- a/metadata/entries/Berlekamp_Zassenhaus.toml +++ b/metadata/entries/Berlekamp_Zassenhaus.toml @@ -1,56 +1,57 @@ title = "The Factorization Algorithm of Berlekamp and Zassenhaus" date = 2016-10-14 topics = [ "Mathematics/Algebra", ] abstract = """
We formalize the Berlekamp-Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun’s square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials.
The algorithm first performs a factorization in the prime field GF(p) and then performs computations in the integer ring modulo p^k, where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using Isabelle’s recent addition of local type definitions.
Through experiments we verify that our algorithm factors polynomials of degree 100 within seconds.
""" license = "bsd" note = "" [authors] [authors.divason] homepage = "divason_homepage" [authors.joosten] email = "joosten_email" [authors.thiemann] email = "thiemann_email" [authors.yamada] email = "yamada_email" [contributors] [notify] thiemann = "thiemann_email" [history] +2024-04-12 = "Added interface to simplify usage of generated code.
As side products, we developed division algorithms for polynomials over integral domains,
as well as primality-testing and prime-factorization algorithms for integers."""
license = "bsd"
note = ""
[authors]
[authors.thiemann]
email = "thiemann_email"
[authors.yamada]
email = "yamada_email"
[contributors]
[notify]
thiemann = "thiemann_email"
yamada = "yamada_email1"
[history]
+2024-04-12 = "changed definition of square-free-factorization.
"
[extra]
[related]