[FOM] Re: Automatic theorem proving in trigonometry and synthetic geometry

[Timothy Y. Chow]

On Thu, 22 Jul 2004, Jeremy Clark wrote:
> Having thought further, I now see that the trigonometric case that I
> have been ham-fistedly blundering towards generalises to the geometric
> case: so the answer is, yes: your geometry problem *can* be blindly fed
> into a computer,

Thanks for your comments.  The information that you (and others like Mitch
Harris) have provided answers the question as I stated it, but now that I
see these answers, I realize that I didn't make myself sufficiently clear
in the first place.  What I was trying to ask about was not the
decidability of the theories in question, but our ability to find proofs
of a certain type.

For the case of "synthetic proofs," I gather from the answers so far that 
the answer is "no, there is no such program available," and this surprises
me somewhat, because I seem to recall that even the popular science 
literature reported many years ago that one of the early successes of
automated reasoning was to find a few unexpected synthetic proofs of
facts of Euclidean geometry.  I also seem to recall a talk I heard 5-10
years ago about some system that would prove theorems of Desargues and
Pappus and the like; maybe this has evolved into the Groebner basis
algorithms that someone mentioned.  I can imagine that a Groebner basis
algorithm with a suitable "front end" that lets you describe a geometric
problem in geometric language (without having to convert it to an 
algebraic statement yourself first) might be close to what I am 
envisioning.

In the case of trigonometry, what I was envisioning was something that
would generate proofs that rely only on a small, fixed set of
trigonometric identities to transform one expression into another.
It could be that the method you described, involving factorization
of polynomials, might provide the basis for such a proof generator,
but I don't think that this follows immediately.  Also, although I
didn't give an example of this, I also had in mind trigonometric
identities with a "side condition," e.g., proving that "X = Y" given
that sin A + sin B = 1.  Presumably these also yield to "algebraic"
techniques, but they might make it harder to devise (or even give a
rigorous definition of) "proofs by identities."

Tim