A verified implementation of the Berlekamp-Zassenhaus factorization algorithm

DOI10.1007/s10817-019-09526-yzbMath1469.68165OpenAlexW2951586102WikidataQ91740323 ScholiaQ91740323MaRDI QIDQ1984794

Akihisa Yamada, Jose Divasón, René Thiemann, Sebastiaan J. C. Joosten

Publication date: 7 April 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-019-09526-y

zbMATH Keywords

theorem provingpolynomial factorizationIsabelle/HOLHensel liftingfactor boundslocal type definitions

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Polynomials, factorization in commutative rings (13P05) Computational methods for problems pertaining to field theory (12-08) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL, From types to sets by local type definition in higher-order logic, Comprehending Isabelle/HOL’s Consistency, A verified implementation of the Berlekamp-Zassenhaus factorization algorithm, A verified implementation of algebraic numbers in Isabelle/HOL, Trustworthy Graph Algorithms (Invited Talk), Classification of finite fields with applications, A formalization of the Smith normal form in higher-order logic

Uses Software

• Maple
• Mathematica
• Isabelle/HOL
• Locales
• Transfer
• Lifting
• Berlekamp Zassenhaus
• Archive Formal Proofs
• Vector Spaces
• Sqrt_Babylonian

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Factoring polynomials and the knapsack problem
• Computing the measure of a polynomial
• Factoring polynomials with rational coefficients
• Isabelle/HOL. A proof assistant for higher-order logic
• Foundational (co)datatypes and (co)recursion for higher-order logic
• From types to sets by local type definition in higher-order logic
• A formalization of the LLL basis reduction algorithm
• Fast machine words in Isabelle/HOL
• Bounds on factors in \(\mathbb Z[x\)]
• The HOL Light theory of Euclidean space
• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
• Locales: a module system for mathematical theories
• Formally verified certificate checkers for hardest-to-round computation
• On Hensel factorization. I
• Algebraic Numbers in Isabelle/HOL
• Modern Computer Algebra
• Verified Indifferentiable Hashing into Elliptic Curves
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Code Generation via Higher-Order Rewrite Systems
• A New Algorithm for Factoring Polynomials Over Finite Fields
• An Inequality About Factors of Polynomials
• A Verified Efficient Implementation of the LLL Basis Reduction Algorithm