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

[Timothy Y. Chow]

Mitch Harris has provided me with numerous useful pointers on this
subject, and I feel that I've collected enough information to give an
update.

I highly recommend the chapter entitled, "Automated reasoning in geometry"  
by Shang-Ching Chou and Xiao-Shan Gao in the "Handbook of Automated
Reasoning" (Elsevier, 2001), Vol. 1, Chapter 11.  Almost everything
mentioned in this thread, except possibly for some of the comments about
trigonometry, is surveyed in this article.  It divides the field into
three subfields:

1. algebraic approaches (Groebner bases, Tarski-Seidenberg-Collins,
Wu-Ritt characteristic sets);

2. coordinate-free approaches (bracket algebras [Cinderella falls into
this category], Clifford algebras, the area method); and

3. AI methods (Gelernter [the pioneer whose machine gave the interesting
pons asinorum proof which I vaguely alluded to before], automated diagram
generating, and others).

Approach 1 is the most powerful as far as having complete decision
procedures goes; the other two approaches either have more limited scope
or don't guarantee that you'll get a solution.  However, approach 1 tends
to yield long, non-human-readable proofs.  For what I was asking about,
approach 2 seems to be the most relevant.  In particular, the "area
method" and its relatives might be the most promising candidate for the
sample problem I posed initially (finding synthetic "high-school-style"
proofs for adventitious angle problems).

The area method was pioneered by J.-Z. Zhang in 1992, who (to quote the 
article) "found many elegant ad hoc methods based on areas of triangles
to solve geometric problems when he was a middle school teacher and
trainer of the Chinese Mathematical Olympiad Team.  These ad hoc methods
have been developed into a complete method ... [that is] surprisingly
powerful in that it has been used to prove hundreds of geometry theorems
of constructive type and the proofs are generally short and elegant."
A major reference is the book by S.-C. Chou, X.-S. Gao, and J.-Z. Zhang, 
"Machine Proofs in Geometry," World Scientific, 1994.  Their program is 
called "Geometry Expert"; see

  http://www.cs.wichita.edu/~chou/ge.html

I haven't [yet] gone as far as to investigate how Geometry Expert handles
adventitious angle problems, but it would be interesting to do so.
Although all adventitious quadrilaterals have been enumerated/classified,
I'm not sure whether anyone has systematically generated synthetic proofs
for them all yet.

By the way, if you're interested in a synthetic solution to the problem I
initially posed, Matthew Frank pointed me to one reference: "Geometry
Civilized" by John Heilbron (it's the last problem in the book).  Also,
I posted the problem to USENET and Yuzuru Hiraga gave an elegant proof,
better than the one in Heilbron's book in my opinion.

http://www.google.com/groups?selm=b7099cae.0407210625.52c130c6%40posting.google.com

Hiraga reflects E in the axis of symmetry of triangle ABC to get E' on 
side AB, and constructs F on line AC such that CE' = CF.  Then one shows
that CD bisects angle E'DF, that triangle E'DF is therefore equilateral;
thus triangle FE'E is isosceles, and so is triangle DE'E.

Turning now to the question of proving trigonometric identities by
appealing only to "high-school identities," I did not find anything
directly relevant during my cursory reading of Chou and Gao's article.
So I don't know yet whether any significant effort has been applied in
this direction.  Mitch Harris asked if I had a list of sample problems.
I have some, in an obscure book by M. T. Liu, "Higher Mathematics for
CU and GCE Matriculation," vol. 1, new ed., Chiu Ming Publishing Co.,
Ltd., Kowloon, Hong Kong, 1977.  This is a Hong Kong secondary school
textbook with some rather difficult problems in it, e.g.,

 -  If A+B+C = pi, prove that cos(B+C-A) + cos(C+A-B) + cos(A+B-C) = 
     3 cos(A) cos(B) cos(C) + (sin^2(A) + sin^2(B) + sin^2(C))/2.

 -  If arctan(x) + arctan(y) + arctan(z) = pi, prove that
     arctan(1/x) + arctan(1/y) + arctan(1/z) = pi/2.

 -  Prove that cos(71) sin(94) + sin(40) cos(93) - cos(31) cos(74) +
     sin(15) sin(52)  =  (sqrt(6) - sqrt(2))/4  [angles in degrees].

 -  Find sin(20) sin(40) sin(60) sin(80) [angles in degrees].

Automatic generation of short and "purely trigonometric" solutions of
these problems seems like a nontrivial task.

Tim