A Verified Implementation of Algebraic Numbers in Isabelle/HOL

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

Descripción completa

Detalles Bibliográficos
Autores principales: Joosten, Sebastiaan J. C., Thiemann, René, Yamada, Akihisa
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Springer Netherlands 2018
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7089722/
https://www.ncbi.nlm.nih.gov/pubmed/32226180
http://dx.doi.org/10.1007/s10817-018-09504-w

Internet

https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7089722/
https://www.ncbi.nlm.nih.gov/pubmed/32226180
http://dx.doi.org/10.1007/s10817-018-09504-w

Ejemplares similares