Skip to main content


Weitere Artikel dieser Ausgabe durch Wischen aufrufen

09.12.2018 | Ausgabe 3/2020 Open Access

Journal of Automated Reasoning 3/2020

A Verified Implementation of Algebraic Numbers in Isabelle/HOL

Journal of Automated Reasoning > Ausgabe 3/2020
Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
Wichtige Hinweise
This research was supported by the Austrian Science Fund (FWF) project Y757. The authors are listed in alphabetical order regardless of individual contributions or seniority. Sebastiaan is now working at University of Twente, the Netherlands, and Akihisa at National Institute of Informatics, Japan. We thank the reviewers of this paper for their helpful comments.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.


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.
Über diesen Artikel

Weitere Artikel der Ausgabe 3/2020

Journal of Automated Reasoning 3/2020 Zur Ausgabe

Premium Partner