Superfluous S-polynomials in Strategy-Independent Grobner Bases

Using the machinery of proof orders originally introduced by Bachmair and Dershowitz in the context of canonical equational proofs, we give an abstract, strategy-independent presentation of Grobner basis procedures and prove the correctness of two classical criteria for recognising superfluous S-polynomials, Buchberger’s criteria 1 and 2, w.r.t. arbitrary fair and correct basis construction strategies. To do so, we develop a general method for proving the strategy-independent correctness of superfluous S-polynomial criteria which seems to be quite powerful. We also derive a new superfluous S-polynomial criterion which is a generalization of Buchberger-1 and is proved to be correct strategy-independently.