I formulated buchberger's Algorithm over certain types of Ore-Algebras, meaning, i have the case $A:=R[y_1,...,y_n]$ with $R$ being a commutative Ring and $y_1,...,y_n$ being noncommutative variables (regarding the Elements of $R$) with the property $y_i y_j=y_j y_i$. Additionally, we demand $deg(y_i f)=deg(y_i)+deg(f)$, with deg being the (multi-)degree of an Element in $f \in A$.
Now, i was able to formulate the Buchberger Algorithm and show its correctness for this case.
My only problem left is to show that it terminates.
In the case of The Algorithm over commutative Polynomial rings, we just had to check the leading term ideals for this, because we knew that an Element $f \in A$ reduced to 0 by Division through $F \subseteq A$ if and only if $lt(f) \in Lt(F)$, with $lt(f)$ being the leading term of $f$ and $lt(F)$ being the Set of leading terms of the (finite) subset of $A$.
Due to that, we knew that by adding elements to $F$ when using the Buchberger Algorithm we also enhanced the Ideal $_A <lm(F)>$, which could only happen finitely often if $A$ was noetherian.
In the noncommutative case, it is very hard to define an equivalent of the leading Term ideal. If we would just use the same Ideal as in the commutative case, we couldn't rule out that there are Elements in the ideal which cannot be obtained by a linear combination of the $lt(f) \in lt(F)$ but by the noncommutative relations and extermination.
I know a way how to define such an ideal in the case of $R$ being a field, and it is definitely possible over such Rings $A$ in which the noncommutative Relation at least does nto change the leading coefficient (however, in the paper I read that which was credible, the proof was omitted).
So, if anyone has a idea how to show the termination of Buchbergers Algorithm in these cases, it would help me quite a lot. In the equivalent of the algorithm i have used, the condition $lc(f) \in _R < \lbrace lc(y^\alpha f) \mid f \in F, deg(f) \in F + \mathbb{N}^n \rbrace>$ was used to check whether an element an be reduced or not.