I've done the same question in math.stackexchange here "https://math.stackexchange.com/questions/1938261/automatic-proof-in-euclidean-geometry-using-theory-of-groebner-bases?noredirect=1#comment3978891_1938261" with meager responses, so for curiosity's sake I posted here in case of some member knows!
Recently, whilst I was reading something in the Theory of Groebner bases, came across the aforementioned question. In the book of Cox, Litlle, O'Shea "Ideals, Varieties and Algorithms" there is a section dealing with that question and some examples, remarks and definitions.
Although, I understand the whole concept and the idea behind all this beautiful application of Groebner bases the general question still is wandering around my head.
Is it feasible to prove everyevery Theorem arises in Euclidean geometry using Groebner bases, in other words, can we produce an algorithm which provides a way to encode everyevery statement in Euclidean Geomtry in terms of polynomials and conclude to the result of hypotheses we've done by answering the ideal membership question for a polynomial? Also, if the latter isn't true, under which circumstances can we have it and what's the general problem? Plays any particular role the number of hypotheses that we have and the number of dependent variables we use to encode the problem? Because seems to be a matter of concern for the writers under the phrase: "...the number of hypotheses and the number of dependent variables are the same. This is typical of properly posed geometric hypotheses."
P.S. Please if you can give me some more information for the above questions like definitions, remarks or references (apart from the aforementioned) would be really helpful