- Abstract:
-
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 Groebner 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 generalisation of Buchberger-1 and is proved to be correct strategy-independently.
- Links To Paper
- 1st Link
- Bibtex format
- @InProceedings{EDI-INF-RR-1343,
- author = {
Grant Passmore
and Leonardo de Moura
},
- title = {Superfluous S-polynomials in Strategy-Independent Groebner Bases},
- book title = {SYNASC-2009 (11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing)},
- publisher = {IEEE Computer Society Conference Publishing Series},
- year = 2009,
- month = {Sep},
- url = {http://research.microsoft.com/en-us/um/people/leonardo/MSR-TR-2009-91.pdf},
- }
|
