Abstract FR:

Dans ce travail, nous etudions la semantique des programmes logiques a l'aide de la logique lineaire. Le premier probleme que nous etudions est celui de la semantique declarative des programmes avec negation dans le corps des clauses, en faisant abstraction de toute strategie de recherche; la methode d'evaluation consideree est sldnf. Nous proposons une theorie logique lineaire, une modification de la completion de clark, comme semantique des programmes autorises allowed. Nous prouvons la correction et la completude de sldnf par rapport a cette semantique. Le deuxieme probleme que nous considerons concerne l'implantation de la methode sldnf specifique a prolog: evaluation des litteraux de la gauche vers la droite, recherche des derivations en profondeur d'abord. Ici, la question de la signification logique de l'operateur not est liee a la question de l'axiomatisation logique du controle. Nous proposons des elements de solution a ce probleme en fournissant une facon d'axiomatiser via la logique lineaire tout programme propositionnel