Reseña: Formalization of a Newton series representation of polynomials
Se ha publicado un artículo de razonamiento formalizado en Coq sobre álgebra titulado Formalization of a Newton series representation of polynomials.
Sus autores son Cyril Cohen y Boris Djalal (del grupo Marelle en Inria Sophia Antipolis, Francia)
Su resumen es
We formalize an algorithm to change the representation of a polynomial to a Newton power series. This provides a way to compute efficiently polynomials whose roots are the sums or products of roots of other polynomials, and hence provides a base component of efficient computation for algebraic numbers. In order to achieve this, we formalize a notion of truncated power series and develop an abstract theory of poles of fractions.
El trabajo se ha presentado en el CPP 2016 (The 5th ACM SIGPLAN Conference on Certified Programs and Proofs).
El código de las correspondientes teorías en Coq se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.