A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
From MaRDI portal
theorem provingIsabelle/HOLpolynomial factorizationHensel liftingfactor boundslocal type definitions
Mechanization of proofs and logical operations (03B35) Polynomials, factorization in commutative rings (13P05) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational methods for problems pertaining to field theory (12-08)
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
- 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?)
- A New Algorithm for Factoring Polynomials Over Finite Fields
- A formalization of the LLL basis reduction algorithm
- 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
- 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
(10)- Comprehending Isabelle/HOL’s Consistency
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- A Macsyma implementation of Zeilberger's fast algorithm
- From types to sets by local type definition in higher-order logic
- A formalization of the Smith normal form in higher-order logic
- Algebraic numbers in Isabelle/HOL
- A verified implementation of algebraic numbers in Isabelle/HOL
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- Classification of finite fields with applications
- Trustworthy Graph Algorithms (Invited Talk)
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)
