You have a bunch of points, lines and circles in some configuration and you have to prove that some condition holds. So you assign symbols to represent the coordinates of each of these points and you represent each fact you are told about them by some equation. The condition you are trying to prove is also represented by some equation. After multiplying up to get rid of square roots each of these equations is setting a polynomial equal to 0. So you are just trying to prove that some polynomial must be 0 if a bunch of other polynomials are 0, which can be done algorithmically via Gröbner bases.
[0] https://mathoverflow.net/questions/337558/automatically-solv...
Grobner it and you are done.
these three points are on one line
these three lines intersect at one point
these two lines are parallel
these four points are on a circle
these two angles are equal
etc ...
There are things that absolutely can be done via coordinates, if one can brute force large algebraic expressions.
Let's say you're given three parallel lines. You can put your x axis along the first line. Then its equation is y = 0. The other two lines necessarily have equations y = a and y = b for some reals a and b. Then you calculate the other quantities involved via a and b and other parameters you have to introduce. At the end you calculate the coordinates of your three points and verify, symbolically, that they lie on the same line.
Yes.
If memory serves right, there's a certain subset of geometry that decidable in that way. Ie you can just run an algorithm.