Automatic proof in Euclidean Geometry using Theory of Groebner Bases 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
 A: Not every theorem in Euclidean geometry can be proven by Gröbner basis methods, because the connection between Gröbner bases and geometry only goes through for algebraic closed fields, such as the complex numbers.  Euclidean plane geometry is defined over the real numbers, so you need a technique that works over the reals.  There such a technique, called quantifier elimination.  You can find some details on Wikipedia here.
In general, both methods can be very slow.  Gröbner bases are known to require doubly exponential time, and quantifier elimination is slower still.  
A: Although I cannot answer your question of whether
every Euclidean geometry theorem can be proved via
Gröbner bases (I doubt it), there is literature on the topic.
Here is one relatively recent source:

Petrovic, Danijela. "Automated Proving in Geometry using Gröbner Bases in Isabelle/HOL." 2011. (PDF download.)


       


And here is an older, highly cited paper:

Kapur, Deepak. "Using Gröbner bases to reason about geometry problems." Journal of Symbolic Computation 2.4 (1986): 399-408.
  (Journal link.)

Abstract excerpt: 
"Two kinds of geometry problems are considered: (i) Given a finite set of geometry relations expressed as polynomial equations, in conjunction with a finite set of subsidiary conditions stated as negations of polynomial equations to rule out certain degenerate eases, check whether another geometry relation expressed as a polynomial equation and given as a conclusion, holds. (ii) Given a finite set of geometry relations expressed as polynomial equations, find a finite set of subsidiary conditions, if any, stated as negations of polynomial equations which rule out certain values of variables, such that another geometry relation expressed as a polynomial equation and given as a conclusion, holds under these conditions."
