Abstract FR:

Le but de cette thèse est de donner des preuves algorithmiques des résultats connus sur les anneaux de Dedekind. La plupart des définitions usuelles se prêtent mal à ce traitement. En effet les questions de factorisation qui sont en théorie considérées comme résolues se heurtent à des problèmes de complexité ou même de décidabilité comme la factorisation du discriminant. Une partie du travail a consisté à donner des preuves constructives plus simples sur les anneaux arithmétiques, en utilisant les matrices de localisation principale. Nous traitons la factorisation des idéaux dans le cadre des anneaux de Prüfer cohérents, et des anneaux de Dedekind, et nous travaillons plus en détail la notion de factorisation partielle qui est pIus facile du point de vue algorithmique. Nous proposons des versions algorithmiques des théorèmes "deux générateurs" et "un et demi" générateur sur les anneaux de Prüfer cohérents de dimension inférieure ou égale à 1, et les anneaux de Dedekind. A la fin nous donnons quelques exemples d'implémentation de certains de nos algorithmes en Axiom.