Jove
Visualize
Contact Us
JoVE
x logofacebook logolinkedin logoyoutube logo
ABOUT JoVE
OverviewLeadershipBlogJoVE Help Center
AUTHORS
Publishing ProcessEditorial BoardScope & PoliciesPeer ReviewFAQSubmit
LIBRARIANS
TestimonialsSubscriptionsAccessResourcesLibrary Advisory BoardFAQ
RESEARCH
JoVE JournalMethods CollectionsJoVE Encyclopedia of ExperimentsArchive
EDUCATION
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab ManualFaculty Resource CenterFaculty Site
Terms & Conditions of Use
Privacy Policy
Policies

Related Concept Videos

Fundamental Theorem of Algebra01:30

Fundamental Theorem of Algebra

146
The Fundamental Theorem of Algebra is central to the study of polynomial equations, asserting that every non-constant polynomial with complex coefficients has at least one complex zero. This means that a polynomial of degree n ≥ 1, written as:  with an ≠ 0, has at least one solution in the complex number system. Since the set of real numbers is a subset of complex numbers, this theorem applies equally to polynomials with real coefficients.Building on this result, the...
146
Real Zeros of Polynomials01:27

Real Zeros of Polynomials

93
Polynomials are algebraic expressions of terms with variables raised to non-negative integer powers. A central aspect of analyzing polynomial functions is determining their real zeros—values of the variable for which the polynomial evaluates to zero. These values represent the x-intercepts of the polynomial’s graph.The Rational Zeros Theorem lists possible rational solutions for a polynomial equation with integer coefficients. If f(x)=anxn+....+a0​, then every rational zero is...
93
Complex Zeros01:29

Complex Zeros

167
Complex zeros are the solutions to polynomial equations that include imaginary numbers, specifically, numbers of the form a + bi, where a and b are real numbers and i is the imaginary unit defined by i2=-1. These zeros satisfy the equation P(x) = 0, where P(x) is a polynomial with real or complex coefficients. Since the complex number system includes all real numbers, it provides a complete framework for analyzing all possible roots of a polynomial.Every polynomial of degree n≥1 can be...
167
Compacting Factor test01:22

Compacting Factor test

472
The compacting factor test is a method used to assess the workability of concrete. It is  especially suitable for concrete mixes containing aggregates up to one and a half inches in size. This test involves specialized equipment consisting of two truncated cone-shaped hoppers and a cylinder, all with polished interior surfaces to minimize friction.
The procedure begins by placing concrete into the upper hopper without any compaction. Once filled, the bottom door of this hopper is opened,...
472
Synthetic Disvision of Polynomials01:28

Synthetic Disvision of Polynomials

88
Synthetic division is an efficient algorithmic approach for dividing a polynomial by a linear binomial of the form x - c, where c is a real number. This method is helpful due to its streamlined process, which avoids the more cumbersome steps involved in the traditional long division of polynomials. It simplifies computation and serves as a practical tool for evaluating polynomials and identifying their factors.To perform synthetic division, one begins by listing the coefficients of the...
88
Long Division of Polynomials01:26

Long Division of Polynomials

159
Polynomial division is an essential algebraic process to simplify expressions and solve equations. Just as numerical division separates a number into quotient and remainder, polynomial long division partitions a polynomial into simpler components; in this context, the dividend is the polynomial being divided, the divisor is the expression dividing it, and the result is expressed in terms of a quotient and a remainder.The division begins by arranging the dividend and divisor in standard...
159

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by
Same author

Intelligent Sensor Software for Robust and Energy-Sustainable Decision-Making in Welding of Steel Reinforcement for Concrete.

Sensors (Basel, Switzerland)·2025
Same author

Analysis of Varroa Mite Colony Infestation Level Using New Open Software Based on Deep Learning Techniques.

Sensors (Basel, Switzerland)·2024
Same author

A Formalization of the Smith Normal Form in Higher-Order Logic.

Journal of automated reasoning·2022
Same author

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL.

Journal of automated reasoning·2020
Same author

A Verified Implementation of Algebraic Numbers in Isabelle/HOL.

Journal of automated reasoning·2020
Same author

Relative Termination via Dependency Pairs.

Journal of automated reasoning·2018

Related Experiment Video

Updated: Dec 24, 2025

A Tactile Automated Passive-Finger Stimulator TAPS
19:44

A Tactile Automated Passive-Finger Stimulator TAPS

Published on: June 3, 2009

14.1K

A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm.

Jose Divasón1, Sebastiaan J C Joosten2, René Thiemann2

  • 11University of La Rioja, Logroño, Spain.

Journal of Automated Reasoning
|April 10, 2020
PubMed
Summary

We present a certified algorithm for factoring integer polynomials using formal verification. This efficient method leverages prime field factorization and modular arithmetic for polynomials up to degree 500.

Keywords:
Factor boundsHensel liftingIsabelle/HOLLocal type definitionsPolynomial factorizationTheorem proving

More Related Videos

Generating Strictly Controlled Stimuli for Figure Recognition Experiments
05:39

Generating Strictly Controlled Stimuli for Figure Recognition Experiments

Published on: March 18, 2019

5.5K

Related Experiment Videos

Last Updated: Dec 24, 2025

A Tactile Automated Passive-Finger Stimulator TAPS
19:44

A Tactile Automated Passive-Finger Stimulator TAPS

Published on: June 3, 2009

14.1K
Generating Strictly Controlled Stimuli for Figure Recognition Experiments
05:39

Generating Strictly Controlled Stimuli for Figure Recognition Experiments

Published on: March 18, 2019

5.5K

Area of Science:

  • Computer Science
  • Formal Methods
  • Computational Algebra

Background:

  • Integer polynomial factorization is a fundamental problem in computational algebra.
  • Formal verification ensures the correctness of algorithms, crucial for mathematical software.
  • Existing algorithms often lack formal guarantees or are inefficient for large polynomials.

Purpose of the Study:

  • To formally verify the Berlekamp-Zassenhaus algorithm for square-free integer polynomials.
  • To adapt Yun's square-free factorization algorithm for integer polynomials.
  • To provide an efficient and certified algorithm for arbitrary univariate polynomial factorization.

Main Methods:

  • Formal verification using the Isabelle/HOL theorem prover.
  • Adaptation of Yun's algorithm for integer polynomials.
  • Implementation using locales and local type definitions due to limitations of dependent types in Isabelle/HOL.
  • Runtime determination of prime field (p) and modulus (k).

Main Results:

  • Successful formal verification of the Berlekamp-Zassenhaus algorithm.
  • An efficient and certified factorization algorithm for univariate integer polynomials.
  • Experimental validation showing factorization of polynomials up to degree 500 within seconds.

Conclusions:

  • The formalized algorithm provides a certified and efficient solution for integer polynomial factorization.
  • The use of locales and local type definitions effectively addresses modeling challenges in Isabelle/HOL.
  • The approach demonstrates the power of formal methods in computational algebra.