Abstract FR:

Les suites de sturm-habicht permettent de determiner le nombre de racines reelles d'un polynome p et les signes d'une liste de polynomes q#1,. . . ,q#k en chacune de ces racines, les polynomes p,q#1,. . . ,q#k etant des polynomes a coefficients reels algebriques. Nous utilisons ces proprietes pour decider si un polynome a n variables et a coefficients entiers admet des racines dans r#+#n et si une inequation polynomiale a plusieurs variables est verifiee pour toute valeur positive ou nulle de ces variables. Nous appliquons ensuite cette methode pour automatiser la preuve de terminaison de systemes de reecriture fondee sur les interpretations polynomiales