A machine-checked implementation of Buchberger's algorithm
We present an implementation of Buchberger's algorithm that has been proved correct within the proof assistant Coq. The implementation contains the basic algorithm plus two standard optimizations.
theorem proving computer algebra grobner bases program verification