A machine-checked implementation of Buchberger's algorithm
scientific article; zbMATH DE number 1565454