Univariate and bivariate integral roots certificates based on Hensel's lifting - Archive ouverte HAL Access content directly
Reports Year :

Univariate and bivariate integral roots certificates based on Hensel's lifting

(1, 2)
1
2

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.
Fichier principal
Vignette du fichier
RRLIP2011-1.pdf (519.44 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

ensl-00575673 , version 1 (11-03-2011)

Identifiers

  • HAL Id : ensl-00575673 , version 1

Cite

Érik Martin-Dorel. Univariate and bivariate integral roots certificates based on Hensel's lifting. 2011. ⟨ensl-00575673⟩
185 View
134 Download

Share

Gmail Facebook Twitter LinkedIn More