Univariate and bivariate integral roots certificates based on Hensels liftingReportar como inadecuado

Univariate and bivariate integral roots certificates based on Hensels lifting - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

* Corresponding author 1 ARENAIRE - Computer arithmetic Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l-Informatique du Parallélisme 2 ARENAIRE - Arithmétique des ordinateurs ENS Lyon - École normale supérieure - Lyon

Abstract : If it is quite easy to check a given integer is a root of a given polynomial with integer coefficients, verifying we know all the integral roots of a polynomial requires a different approach. In both univariate and bivariate cases, we introduce a type of integral roots certificates and the corresponding checker specification, based on Hensel-s lifting. We provide a formalization of this iterative algorithm from which we deduce a formal proof of the correctness of the checkers, with the help of the COQ proof assistant along with the SSReflect extension. The ultimate goal of this work is to provide a component that will be involved in a complete certification chain for solving the Table Maker-s Dilemma in an exact way.

Keywords : Coq formal proofs Certifying algorithm Hensel-s lifting Integral roots Polynomials

Autor: Érik Martin-Dorel -

Fuente: https://hal.archives-ouvertes.fr/


Documentos relacionados