This thesis considers the correctness and termination of two Gröbner basis algorithms. After developing the theory of Gröbner bases, reviewing standard efficiencies, and giving an example of their use, we examine a revised Staggered Linear Basis algorithm and the F₅ algorithm.

The revised Staggered Linear Basis algorithm, given by Mora as an instructive example, includes a small modification of the original algorithm. We establish by counterexample that it does not always terminate, and give a rigorous proof of its correctness if it does terminate. We also show that the original Staggered Linear Basis algorithm is not correct.

Faugère's F₅ algorithm appears to be faster than previous algorithms for computing Gröbner bases. As of this writing, a few demonstration implementations exist, but efficient, compiled implementations are still not widely available. Its correctness has been proven, which we show, but its termination is an open question, which we discuss.

Finally, we make some observations on tests performed with the algorithms. In particular, we observe that two published versions of the CritPair subroutine of F₅ compute the same number of polynomials, leading to a conjecture that certain pairs that are not normalized are also rewritable.