Back to Search
Start Over
A Verified Implementation of Algebraic Numbers in Isabelle/HOL
- Source :
- Journal of Automated Reasoning
- Publication Year :
- 2018
- Publisher :
- Springer Science and Business Media LLC, 2018.
-
Abstract
- We formalize algebraic numbers in Isabelle/HOL. Our development serves as a verified implementation of algebraic operations on real and complex numbers. We moreover provide algorithms that can identify all the real or complex roots of rational polynomials, and two implementations to display algebraic numbers, an approximative version and an injective precise one. We obtain verified Haskell code for these operations via Isabelle's code generator. The development combines various existing formalizations such as matrices, Sturm's theorem, and polynomial factorization, and it includes new formalizations about bivariate polynomials, unique factorization domains, resultants and subresultants.
- Subjects :
- Computer science
Unique factorization domain
HOL
0102 computer and information sciences
02 engineering and technology
01 natural sciences
Article
Resultants
Real algebraic geometry
Artificial Intelligence
ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION
0202 electrical engineering, electronic engineering, information engineering
Algebraic number
Theorem proving
computer.programming_language
020207 software engineering
Algebraic numbers
Algebra
Computational Theory and Mathematics
010201 computation theory & mathematics
Factorization of polynomials
Algebraic operation
Haskell
computer
Complex number
Software
Subjects
Details
- ISSN :
- 15730670 and 01687433
- Volume :
- 64
- Database :
- OpenAIRE
- Journal :
- Journal of Automated Reasoning
- Accession number :
- edsair.doi.dedup.....772adda11cd79e29aa724e006382ee92