[FOM] Automatic theorem proving in trigonometry and synthetic geometry

[Mitchell Harris]

On Wed, 21 Jul 2004, Timothy Y. Chow wrote:

>The reason I bring this up on FOM is that I am wondering whether the state
>of the art in automated theorem proving is such that this kind of problem
>can be (more-or-less blindly) fed to a program that will solve it.  
...
>Related question:
>If I decide to tackle the problem by hand using trigonometry and find 
>myself needing to prove (say) that tan(50) = tan(20)/(1-4sin(10)), do I
>have to think or can a machine generate the proof for me?

- "elementary geometry" is solvable using Groebner basis completion. This
is questionably synthetic in that it doesn't use numerical operations (on
floating point numbers with rounding), but it is algebraic (requires a
translation to a multivariate system of polynomials. Zeilberger has a set
of examples of geometric theorems proved this way, with the most difficult
being Morley's theorem (about trisectors of the angles of a triangle
forming an equilateral triangle), that are proven automatically (using
Maple). 

- there is a system for proving trigonometric identities (with certain 
restrictions): convert to exponentials with a normal form ordered by 
exponents.

- I don't think there is a current logical system for doing proofs
synthetically (like Euclid). Geometry software (like Geometer's Sketchpad,
or Cinderella) "prove" conjectures by numeric example (modify the free
objects, check the conjectures object properties numerically, report true
if below a small epsilon).

-- 
Mitch Harris
Lehrstuhl fuer Automatentheorie, Fakultaet Informatik
Technische Universitaet Dresden, Deutschland
http://lat.inf.tu-dresden.de/~harris