j\leq s}{\rm NTObs}(i,j)$.

-   If $B=\emptyset$, return the result ${G}$. Otherwise, select an obstruction ${\rm o}_{i,j}(w_{i},w'_{i};$ $w_{j},w'_{j})\in B$ using a fair strategy and delete it from $B$.

-   Compute the S-polynomial $S=S_{i,j}(w_{i},w'_{i};w_{j},w'_{j})$ and its normal remainder $S'={\rm NR}_{\sigma,G}(S)$. If $S'=0$, continue with step [(B2)]{}.

-   Increase $s$ by one, append $g_{s}=S'$ to the set ${G}$, and append the set of obstructions $\bigcup_{1\leq i\leq s}{\rm NTObs}(i,s)$ to the set $B$. Then continue with step [(B2)]{}.

This is a procedure that enumerates a ${\sigma}$-Gröbner basis ${G}$ of $I$. If $I$ has a finite ${\sigma}$-Gröbner basis, the procedure stops after finitely many steps and the resulting set ${G}$ is a finite ${\sigma}$-Gröbner basis of $I$.

Note that this is a straightforward generalization of the commutative version of Buchberger’s algorithm to the non-commutative case. We refer to [@Mo94] for the original form of this procedure and to [@Xiu12], Theorem 4.1.14 for a detailed proof.

Non-Commutative Gebauer-Möller Criteria {#sec3}
=======================================

In this section we present non-commutative Gebauer-Möller criteria. They check whether an obstruction can be represented by “smaller” obstructions. If so, we declare such obstructions to be *unnecessary*. Before going into details, we define a certain well-ordering $\tau$ on $\mathbb{T}(F_{s})=\{we_{i}w'\ |\ i\in\{1,\dots,s\}, w,w'\in\langle X\rangle\}$ and 