The leading term in a non-zero multivariate polynomial is the term of the polynomial’s degree in the polynomial. The leading term in the zero polynomial is defined as the zero polynomial.

Given a multivariate polynomial \(p\) and a set \(B\) of multivariate polynomials over a commutative semiring \(R\), and a monomial order. If there exists a \(g : B \to R[X]\) with finite support, and a multivriate polynomial \(r\), such that

1. \(p = \sum _{b\in B} g(b)b + r,\)

2. degree of any non-zero \(g(b)b\) where bB is less than or equal to the degree of \(p\),

3. none of terms of \(r\) is divisible by leading monomial of a non-zero elements of \(B\),

then \(r\) is called a remainder of \(p\) on division by “divisors” \(B\).

A statement that r is a remainder of p on division by B w.r.t. a monomial order m is denoted as m.IsRemainder p B r.

Fix a monomial order on the polynomial ring \(k[x_1, \ldots , x_n]\).A finite subset \(G = \{ g_1, \ldots , g_t\} \) of an ideal \(I \subseteq k[x_1, \ldots , x_n]\), with \(I \ne \{ 0\} \), is said to be a Gröbner basis (or standard basis) if

Using the convention that \(\langle \emptyset \rangle = \{ 0\} \), we define the empty set \(\emptyset \) to be the Gröbner basis of the zero ideal \(\{ 0\} \).

The \(S\)-polynomial of \(f\) and \(g\) is the combination