@INPROCEEDINGS{BachmairGanzinger-94-ccl,                      
        AUTHOR = {Bachmair, L. and Ganzinger, H.},
        BOOKTITLE = {1st International Conference on Constraints in
Computational Logics},
        TITLE = {Buchberger's algorithm: a constraint-based completion procedure},
        YEAR = {1994},
	PAGES = {285--301},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = {845},
	PUBLISHER = {Springer-Verlag},
        abstract = {
We present an extended completion procedure with built-in theories
defined by a collection of associativity and commutativity axioms
and additional ground equations,
and reformulate Buchberger's algorithm for constructing
Gr\"obner bases for polynomial ideals in this formalism.
The presentation of completion is at an abstract level,
by transition rules,
with a suitable notion of fairness used to characterize
a wide class of correct completion procedures,
among them Buchberger's original algorithm
for polynomial rings over a field.
},
}