Search research articles

ABOUT JoVE

Overview Leadership Blog JoVE Help Center

AUTHORS

Publishing Process Editorial Board Scope & Policies Peer Review FAQ Submit

LIBRARIANS

Testimonials Subscriptions Access Resources Library Advisory Board FAQ

RESEARCH

JoVE Journal Methods Collections JoVE Encyclopedia of Experiments Archive

EDUCATION

JoVE Core JoVE Business JoVE Science Education JoVE Lab Manual Faculty Resource Center Faculty Site

Terms & Conditions of Use

Related Concept Videos

Fundamental Theorem of Algebra

Fundamental Theorem of Algebra

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...

Algebraic Expressions

Algebraic Expressions

Algebraic expressions are essential in mathematics. They represent relationships through variables, constants, and operations. These expressions help describe patterns and solve problems in various mathematical fields. Understanding their components, classifications, and operations allows for efficient simplification and manipulation.Each algebraic expression consists of individual parts, including numbers and symbols, that work together to form meaningful mathematical statements. The numerical...

SFG Algebra

SFG Algebra

In Signal Flow Graph (SFG) algebra, the value a node represents is determined by the sum of all signals entering that node. This summed value is then transmitted through every branch leaving the node, making the SFG a powerful tool for visualizing and analyzing control systems.
Each node in an SFG corresponds to a variable, and the interactions between nodes are represented by branches with associated gains. When multiple branches lead into a node, the value at that node is the sum of the...

Real Number Operations

Real Number Operations

The concept of real numbers includes all the values that can be represented on a continuous number line. The system began with basic counting values used for enumeration. It later expanded to include values that represent the absence of quantity and opposites of the counting values. When situations required expressing parts of a whole or dividing quantities evenly, values capable of representing such proportions were developed. When written using decimal notation, these values can end or repeat...

The Intermediate Value Theorem

The Intermediate Value Theorem

The Intermediate Value Theorem is a foundational result in calculus that guarantees the existence of solutions within certain intervals for continuous functions. Formally, the Intermediate Value Theorem states that if a function f is continuous on the closed interval [a, b], and if N is any value between f(a) and f(b), then there exists at least one c ∈ (a, b) such that f(c) = N. This theorem is instrumental in proving the existence of roots and in analyzing the behavior of continuous...

Quadratic Equations in the Complex Number System

Quadratic Equations in the Complex Number System

A quadratic equation in the form ax2+bx+c=0 can have solutions that vary in nature depending on the value of the discriminant, b2−4ac. In this expression, a is the coefficient of the quadratic term x2, b is the coefficient of the linear term x, and c is the constant term. When the discriminant is negative, the equation has no real number solutions. However, by introducing complex numbers through the imaginary unit i, defined by i=-1, these equations can still be solved.The square root of...

You might also read

Related Articles

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

Sort by

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 the Berlekamp-Zassenhaus Factorization Algorithm.

Journal of automated reasoning·2020

Same author

Relative Termination via Dependency Pairs.

Journal of automated reasoning·2018

Search research articles

Related Experiment Video

Updated: Dec 25, 2025

Generation and Coherent Control of Pulsed Quantum Frequency Combs

Generation and Coherent Control of Pulsed Quantum Frequency Combs

Published on: June 8, 2018

A Verified Implementation of Algebraic Numbers in Isabelle/HOL.

Sebastiaan J C Joosten¹, René Thiemann¹, Akihisa Yamada¹

¹University of Innsbruck, Innsbruck, Austria.

Journal of Automated Reasoning

|April 1, 2020

Summary

This study formalizes algebraic numbers and their operations in Isabelle/HOL, providing verified algorithms for root finding and number display. Verified Haskell code is generated for these essential mathematical computations.

Keywords:

Algebraic numbers Real algebraic geometry Resultants Theorem proving

More Related Videos

Multimedia Battery for Assessment of Cognitive and Basic Skills in Mathematics BM-PROMA

Multimedia Battery for Assessment of Cognitive and Basic Skills in Mathematics BM-PROMA

Published on: August 28, 2021

Generating Strictly Controlled Stimuli for Figure Recognition Experiments

Generating Strictly Controlled Stimuli for Figure Recognition Experiments

Published on: March 18, 2019

Related Experiment Videos

Last Updated: Dec 25, 2025

Generation and Coherent Control of Pulsed Quantum Frequency Combs

Generation and Coherent Control of Pulsed Quantum Frequency Combs

Published on: June 8, 2018

Multimedia Battery for Assessment of Cognitive and Basic Skills in Mathematics BM-PROMA

Multimedia Battery for Assessment of Cognitive and Basic Skills in Mathematics BM-PROMA

Published on: August 28, 2021

Generating Strictly Controlled Stimuli for Figure Recognition Experiments

Generating Strictly Controlled Stimuli for Figure Recognition Experiments

Published on: March 18, 2019

Area of Science:

Formal verification
Computational algebra
Number theory

Background:

Formalization of mathematical concepts is crucial for reliable software.
Algebraic numbers and their operations are fundamental in mathematics.
Existing formalizations lacked comprehensive algebraic number support.

Purpose of the Study:

To formalize algebraic numbers and their operations in Isabelle/HOL.
To develop verified algorithms for finding roots of polynomials.
To generate executable code for algebraic number computations.

Main Methods:

Utilized Isabelle/HOL for formal verification.
Integrated existing formalizations (matrices, Sturm's theorem, polynomial factorization).
Developed new formalizations for bivariate polynomials, UFDs, resultants, and subresultants.

Main Results:

Formalized algebraic numbers and verified their arithmetic operations.
Provided algorithms to identify all real and complex roots of rational polynomials.
Created two implementations for displaying algebraic numbers: approximate and precise injective.

Conclusions:

The development provides a verified foundation for algebraic number computations.
Generated verified Haskell code for algebraic number operations and root finding.
The work advances formal methods in computational algebra and number theory.