Standard bases for general coefficient rings and a new constructive proof of Hilbert's basis theorem

A constructive proof is given of the termination of the algorithm for computing standard bases in polynomial rings over a “constructively noetherian” ring. A new constructive version of the noetherian chain condition is introduced and Hilbert's basis theorem is proved with this new condition and the construction of standard bases