Skip to main content
main-content

Tipp

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

Zeitschrift:
Journal of Automated Reasoning > Ausgabe 3/2020
Autoren:
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.

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.

Unsere Produktempfehlungen

Premium-Abo der Gesellschaft für Informatik

Sie erhalten uneingeschränkten Vollzugriff auf alle acht Fachgebiete von Springer Professional und damit auf über 45.000 Fachbücher und ca. 300 Fachzeitschriften.

Literatur
Über diesen Artikel

Weitere Artikel der Ausgabe 3/2020

Journal of Automated Reasoning 3/2020 Zur Ausgabe

Premium Partner

    Bildnachweise