Abstract FR:

Nous presentons dans un premier temps une classe d'applications entre langages de programmations par contraintes, appelees approximations. Ceci nous autorise a nous concentrer sur les images pq et pb d'un programme p dans le domaine des rationnels positifs et celui des booleens. L'etude de pq nous permet de mettre a jour des termes lineaires decroissants a chaque appel de celle de pb nous renseigne sur l'etat des variables apres succes. Finalement, a partir de ces deux informations, nous calculons les conditions minimales garantissant la terminaison des preuves pour un systeme prolog de toute requete satisfaisant ces conditions