Related Experiment Video
Updated: Dec 25, 2025
06:42
Generation and Coherent Control of Pulsed Quantum Frequency Combs
Published on: June 8, 2018
9.6K
A Verified Implementation of Algebraic Numbers in Isabelle/HOL
Sebastiaan J C Joosten1, René Thiemann1, Akihisa Yamada1
1University 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.
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.
Related Concept Videos
01:30Fundamental Theorem of Algebra
147
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...
147
01:26Algebraic Expressions
186
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...
186
01:16SFG Algebra
267
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...
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...
267
01:27Real Number Operations
179
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...
179
01:25The Intermediate Value Theorem
148
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...
148
01:29Quadratic Equations in the Complex Number System
210
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...
210