\[sec2pro10\]), and formulate the Buchberger Procedure (see Theorem \[sec2the11\]). The non-commutative analogues of the Gebauer-Möller criteria are developed in Section \[sec3\]. They are based on a careful study of the set of newly constructed obstructions which are produced during the execution of Buchberger’s Procedure. As a result, we are able to formulate the Non-Commutative Multiply Criterion (see Proposition \[ncMCrit\]), the Non-Commutative Leading Word Criterion (see Proposition \[ncLWCrit\]) and the Non-Commutative Backward Criterion (see Proposition \[ncBKCrit\]). When we combine these criteria, the result is a new Improved Buchberger Procedure \[sec3the14\].

The second author has implemented a version of the Buchberger Procedure for non-commutative polynomial rings in a package for the computer algebra system [ApCoCoA]{} which includes the non-commutative Gebauer-Möller criteria developed here (see [@Ap10]). In the last section, we present experimental results about the efficiency of the criteria for some cases of moderately difficult Gröbner basis computations.

Unless mentioned otherwise, we adhere to the definitions and terminology given in [@KR00] and [@KR05].

Gröbner Bases in $K\langle X\rangle$ {#sec2}
====================================

In the following we let $X=\{x_1,\dots,x_n\}$ be a finite set of indeterminates (or a finite alphabet), and $\langle X\rangle$ the monoid of all *words* (or *terms*) $x_{i_1}\cdots x_{i_l}$ where the multiplication is 