One of the aims of Constructive Mathematics is to provide effective methods (algorithms) to compute objects whose existence is asserted by Classical Mathematics. Moreover, all proofs should be constructive, i.e., have an underlying effective content. E.g. the classical proof of the correctness of Buchberger algorithm, based on noetherianity, is non constructive~: the closest consequence is that we know that the algorithm \ ends, but we don't know when.
In this paper we explain how the Buchberger algorithm can be used in order to give a constructive approach to the Hilbert basis theorem and more generally to the constructive content of ideal theory in polynomial rings over "discrete" fields .
More precisely we give a constructive version of Dickson's Lemma, we deduce constructively the correctness of Buchberger algorithm and from this result we get the Hilbert basis theorem in a constructive form.
Nous donnons une version constructive du lemme de Dickson. Nous en déduisons une preuve constructive de correction pour l'algorithme de Buchberger. Nous obtenons comme conséquence une version constructive du théorème "de la base" de Hilbert dans les anneaux de polynomes sur un corps "discret".