| This thesis considers the correctness and termination of two Grobner basis algorithms. After developing the theory of Grobner bases, reviewing standard efficiencies, and giving an example of their use, we examine a revised Staggered Linear Basis algorithm and the F5 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.;Faugere's F5 algorithm appears to be faster than previous algorithms for computing Grobner 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 F5 compute the same number of polynomials, leading to a conjecture that certain pairs that are not normalized are also rewritable. |
