Cargando…
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...
Autores principales: | Joosten, Sebastiaan J. C., Thiemann, René, Yamada, Akihisa |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
Springer Netherlands
2018
|
Materias: | |
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 |
Ejemplares similares
-
Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL
por: Thiemann, René, et al.
Publicado: (2020) -
Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL
por: Bottesch, Ralph, et al.
Publicado: (2020) -
Algebraically Closed Fields in Isabelle/HOL
por: de Vilhena, Paulo Emílio, et al.
Publicado: (2020) -
Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
por: Guttmann, Walter
Publicado: (2020) -
A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm
por: Divasón, Jose, et al.
Publicado: (2019)