Abstract FR:

Formalisation, preuve et differences extensions de la methode d'alexandre. Son algorithme, les preuves de terminaison, correction et completude sont proposes. L'extension de la methode aux programmes avec negation stratifies est etudiee