The fundamental fact about Gröbner bases is that they exist; and, as shown by basic work of Buchberger, they are effectively computable for fields K of practical importance, by a simple if possibly long-winded elimination method. The main theoretical burden of the work is the correctness of Buchberger's algorithm: that is, it is known to terminate in a Gröbner basis.
In detail, given initially a finite set of generators for the ideal I, we can take any two, P and Q, and add to our list MP - NQ where M and N are monomials chosen to make the top term in that combination cancel. We can decide what is the top term by some ordering of lexicographic type (X > Y > Z, say); choice of the ordering gives some computational flexibility. Once that is done, once and for all, the monomials M and N are determinate up to possible constants, by an obvious recipe: for example to make top terms X2Y3 and XY7 cancel we multiply the first by M = Y4 and the second by N = X, and subtract.
The algorithm is then simply to saturate the list: eventually 'nothing new' will result. This generalises the Euclidean algorithm, for polynomials in one variable, where one of M and N can always be taken as 1, and the degree always goes down (hence we shall reach an end point). In this case termination comes out of the so-called Dickson's lemma.
The Gröbner basis algorithm can certainly be slow to terminate in the worst case; but is of practical use.