[isabelle] yet another AFP entry: Algebraic Numbers in Isabelle/HOL



Today we have an embarrassment of riches in the form of a third, and substantial, AFP entry. Abstract:

"Based on existing libraries for matrices and Sturm's theorem, we formalized algebraic numbers in Isabelle/HOL. Our development serves as an implementation for real and complex numbers, and it admits to compute roots and completely factorize rational, real, and complex polynomials, provided that all coefficients are rational numbers. Moreover, we provide two implementations to display algebraic numbers, an injective and expensive one, or a faster but approximative version.â

The full entry is here:

http://afp.sourceforge.net/entries/Algebraic_Numbers.shtml

Once again, many thanks to the authors!

Larry Paulson






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.