[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:


Once again, many thanks to the authors!

Larry Paulson

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