A Verified Implementation of Algebraic Numbers in Isabelle/HOL

Sebastiaan J.C. Joosten; René Thiemann; Akihisa Yamada

doi:10.1007/s10817-018-09504-w

A Verified Implementation of Algebraic Numbers in Isabelle/HOL

Sebastiaan J.C. Joosten, René Thiemann^* (Corresponding Author), Akihisa Yamada

^*Corresponding author for this work

Research output: Contribution to journal › Article › Academic › peer-review

3 Citations (Scopus)

25 Downloads (Pure)

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.

Original language	English
Pages (from-to)	363-389
Number of pages	27
Journal	Journal of automated reasoning
Volume	64
Early online date	9 Dec 2018
DOIs	https://doi.org/10.1007/s10817-018-09504-w
Publication status	Published - Mar 2020
Externally published	Yes

Keywords

Algebraic numbers
Real algebraic geometry
Resultants
deal
Theorem proving

Access to Document

10.1007/s10817-018-09504-wLicence: CC BY

Joosten2018verifiedFinal published version, 975 KBLicence: CC BY

Cite this

@article{5399b8eaea3440d4bba8d3a066f33e2c,

title = "A Verified Implementation of Algebraic Numbers in Isabelle/HOL",

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{\textquoteright}s code generator. The development combines various existing formalizations such as matrices, Sturm{\textquoteright}s theorem, and polynomial factorization, and it includes new formalizations about bivariate polynomials, unique factorization domains, resultants and subresultants.",

keywords = "Algebraic numbers, Real algebraic geometry, Resultants, deal, Theorem proving",

author = "Joosten, {Sebastiaan J.C.} and Ren{\'e} Thiemann and Akihisa Yamada",

note = "Springer deal",

year = "2020",

month = mar,

doi = "10.1007/s10817-018-09504-w",

language = "English",

volume = "64",

pages = "363--389",

journal = "Journal of automated reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

}

TY - JOUR

T1 - A Verified Implementation of Algebraic Numbers in Isabelle/HOL

AU - Joosten, Sebastiaan J.C.

AU - Thiemann, René

AU - Yamada, Akihisa

N1 - Springer deal

PY - 2020/3

Y1 - 2020/3

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

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

KW - Algebraic numbers

KW - Real algebraic geometry

KW - Resultants

KW - deal

KW - Theorem proving

U2 - 10.1007/s10817-018-09504-w

DO - 10.1007/s10817-018-09504-w

M3 - Article

SN - 0168-7433

VL - 64

SP - 363

EP - 389

JO - Journal of automated reasoning

JF - Journal of automated reasoning

ER -

A Verified Implementation of Algebraic Numbers in Isabelle/HOL

Abstract

Keywords

Access to Document

Fingerprint

Cite this