Abstract FR:

Le but de ce travail est d'etudier deux problemes lies a l'utilisation de la negation en programmation logique avec contraintes: celui ou la negation apparait dans les contraintes et celui ou elle apparait dans le corps des clauses des programmes consideres. Le premier probleme consiste a montrer comment il est possible d'etendre raisonnablement un algorithme de resolution, permettant de mettre des contraintes positives sous forme canonique, aux contraintes niees. Pour cela, nous adaptons le processus deja utilise et nous considerons par ailleurs un operateur de recouvrement adequat. Nous enoncons des conditions suffisantes qui nous permettent alors de definir la forme canonique etendue d'un systeme general de contraintes avec negation. En ce qui concerne le second probleme, nous proposons un nouveau schema de negation constructive, pour les programmes generaux avec contraintes, base sur une modelisation theorique. En outre, nous associons a ces programmes une nouvelle semantique declarative, l'axiomatique interne, qui nous permet d'obtenir un theoreme de completude en deduction classique ordinaire, c'est-a-dire bivaluee