Buchberger-Zacharias Theory of multivariate Ore extensions

Following the recent survey on Buchberger-Zacharias Theory for monoid rings R[S] over a unitary effective ring R and an effective monoid S, we propose here a presentation of Buchberger-Zacharias Theory and related Gröbner basis computation algorithms for multivariate Ore extensions of rings presented as modules over a principal ideal domain, using Möller-Pritchard lifting theorem.