In Is it possible to solve any Euclidean geometry problem using a computer? I claimed that one can convert the statement of a theorem in Euclid into multivariate polynomials such that Groebner basis completion would supply an 'automated' proof:
- an arbitrary point can be represented by two variables $(x,y)$
- a line by two points $(x_1,y_1),(x_2,y_2)$
- a point $(x_3,y_3)$ on a line $(x_1,y_1),(x_2,y_2)$ by $(y3-y_1)(x_2-x_1) = (x_3-x_1)(y_2-y_1)$
- a point on a circle with radius $d$ by $(x_1-x_2)^2 + (y_1-y_2)^2 = d^2$. (and of course the distance itself might be from another definition of a circle.
I left out the additional translation of the 'angle' concept. A large part of Euclid involves use of angles (for example, the angles opposite equal sides of a triangle are equal, or the sum of the interior angles of a triangle is $\pi$).
It should be straightforward to translate an angle into a statement about points. Three points in order somehow represent an angle at the middle point. But I can't figure out how to show that two angles are equal by converting them to polynomials, or show that one angle is half another, etc.
Any ideas?
For "geometric" angles ($180^{\circ}$ or less), two angles are equal precisely if their cosines are equal, and equality of cosines can be expressed algebraically. One can also handle in a similar way the notion of one angle being twice another, or three times another. As to the rest, it all depends on what you mean by the "etc." near the end of your question.