A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
From MaRDI portal
factor boundsHensel liftingIsabelle/HOLlocal type definitionspolynomial factorizationtheorem proving
Mechanization of proofs and logical operations (03B35) Computational methods for problems pertaining to field theory (12-08) Polynomials, factorization in commutative rings (13P05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)
Recommendations
- scientific article; zbMATH DE number 953213
- scientific article; zbMATH DE number 691468
- Improving the algorithms of Berlekamp and Niederreiter for factoring polynomials over finite fields
- Improvements on the Cantor-Zassenhaus factorization algorithm.
- Schemes for deterministic polynomial factoring
- Deterministic verification of integer matrix multiplication in quadratic time
- scientific article; zbMATH DE number 4077312
- Deterministic analysis of aleatoric methods of polynomial factorization over finite fields
- On the Complexity of the Montes Ideal Factorization Algorithm
- A new polynomial factorization algorithm and its implementation
Cites work
- A formalization of the LLL basis reduction algorithm
- A New Algorithm for Factoring Polynomials Over Finite Fields
- A verified efficient implementation of the LLL basis reduction algorithm
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- Algebraic numbers in Isabelle/HOL
- An Inequality About Factors of Polynomials
- Bounds on factors in \(\mathbb Z[x]\)
- Code generation via higher-order rewrite systems
- Computing the measure of a polynomial
- Factoring polynomials and the knapsack problem
- Factoring polynomials with rational coefficients
- Fast machine words in Isabelle/HOL
- Formally verified certificate checkers for hardest-to-round computation
- Foundational (co)datatypes and (co)recursion for higher-order logic
- From types to sets by local type definition in higher-order logic
- scientific article; zbMATH DE number 3785035 (Why is no real title available?)
- scientific article; zbMATH DE number 1052006 (Why is no real title available?)
- scientific article; zbMATH DE number 1065062 (Why is no real title available?)
- scientific article; zbMATH DE number 3265895 (Why is no real title available?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Locales: a module system for mathematical theories
- Modern computer algebra
- On Hensel factorization. I
- The HOL Light theory of Euclidean space
- Verified indifferentiable hashing into elliptic curves
Cited in
(11)- A Macsyma implementation of Zeilberger's fast algorithm
- From types to sets by local type definition in higher-order logic
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- A formalization of the Smith normal form in higher-order logic
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- A verified implementation of algebraic numbers in Isabelle/HOL
- Classification of finite fields with applications
- Algebraic numbers in Isabelle/HOL
- Comprehending Isabelle/HOL’s Consistency
- Trustworthy Graph Algorithms (Invited Talk)
- Derandomization with pseudorandomness
Describes a project that uses
Uses Software
This page was built for publication: A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1984794)
