# 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

• The book of Cox, Little, and O'Shea has references on that matter, did you check them? – Vladimir Dotsenko Sep 27 '16 at 14:23

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.

• It's easy to find more about this topic if you search for automated theorem proving in geometry. It's been active research area pretty much since computers were invented. – arsmath Sep 27 '16 at 15:04
• So can we say that the answer on my question is positive for $\mathbb{C}$ instead of $\mathbb{R}$? That is, can every statement arising in $\mathbb{C}$ from $\mathbb{R}^{2}$ (we are speaking in affine-geometrical terms though) which can be given encoded in polynomial equations, to be solved using Theory of Groebner Bases? – mayer_vietoris Sep 27 '16 at 16:41
• @mayer_vietoris For the purposes of this you can't treat $\mathbb{C}$ as the same as $\mathbb{R}^2$. For example, there's no way to extract the real and complex part of a complex number using only polynomials. Some statements still make sense over the complexes: you can still define point, line, plane, etc. Other concepts don't make sense over the complexes, such as line segment, the interior of a triangle, etc. There will even be some statements that are true over the reals and false over the complex and vice versa (theorems about conics, for example). – arsmath Sep 28 '16 at 13:43

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."

• Thank you very much Joseph, your comment helps me a lot I think! Will pour my "attention" on those two references! – mayer_vietoris Sep 27 '16 at 15:31