A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
type: Item
instance of: scholarly article
title: A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
zbMATH Open document ID: 1469.68165
author: Jose Divasón
author: René Thiemann
author: Akihisa Yamada
author: Sebastiaan J. C. Joosten
published in: Journal of Automated Reasoning
publication date: 2020-04-07T00:00:00Z
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 12-08
Mathematics Subject Classification ID: 13P05
Mathematics Subject Classification ID: 68V20
zbMATH DE Number: 7187044
zbMATH Keywords: factor bounds
zbMATH Keywords: Hensel lifting
zbMATH Keywords: Isabelle/HOL
zbMATH Keywords: local type definitions
zbMATH Keywords: polynomial factorization
zbMATH Keywords: theorem proving
describes a project that uses: Isabelle/HOL
describes a project that uses: Locales
describes a project that uses: Archive Formal Proofs
describes a project that uses: Sqrt_Babylonian
describes a project that uses: Maple
describes a project that uses: Mathematica
describes a project that uses: Lifting
describes a project that uses: Transfer
describes a project that uses: Berlekamp Zassenhaus
describes a project that uses: Vector Spaces
MaRDI profile type: Publication
Wikidata QID: Q91740323
full work available at URL: s10817-019-09526-y
OpenAlex ID: W2951586102
cites work: Bounds on factors in \(\mathbb Z[x]\)
cites work: Q4356368
cites work: Locales: a module system for mathematical theories
cites work: Verified Indifferentiable Hashing into Elliptic Curves
cites work: Q5550483
cites work: Foundational (co)datatypes and (co)recursion for higher-order logic
cites work: A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
cites work: A New Algorithm for Factoring Polynomials Over Finite Fields
cites work: Computing the measure of a polynomial
cites work: A formalization of the LLL basis reduction algorithm
cites work: Code Generation via Higher-Order Rewrite Systems
cites work: The HOL Light theory of Euclidean space
cites work: Factoring polynomials and the knapsack problem
cites work: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
cites work: Q4349924
cites work: From types to sets by local type definition in higher-order logic
cites work: Factoring polynomials with rational coefficients
cites work: Fast machine words in Isabelle/HOL
cites work: Formally verified certificate checkers for hardest-to-round computation
cites work: An Inequality About Factors of Polynomials
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Algebraic Numbers in Isabelle/HOL
cites work: Modern computer algebra
cites work: Q3963124
cites work: On Hensel factorization. I
DOI: 10.1007/S10817-019-09526-Y
Recommended article: Q4718158
Recommended article: Q4314359
Recommended article: Improving the algorithms of Berlekamp and Niederreiter for factoring polynomials over finite fields
Recommended article: Improvements on Cantor-Zassenhaus Factorization Algorithm
Recommended article: Schemes for deterministic polynomial factoring
Recommended article: Deterministic Verification of Integer Matrix Multiplication in Quadratic Time
Recommended article: Q3808150
Recommended article: Deterministic analysis of aleatoric methods of polynomial factorization over finite fields
Recommended article: On the Complexity of the Montes Ideal Factorization Algorithm
Recommended article: A new polynomial factorization algorithm and its implementation
description: scientific article; zbMATH DE number 7187044