[FOM] Automatic theorem proving in trigonometry and synthetic geometry

[Mitchell Harris]

On Thu, 22 Jul 2004, Mitchell Harris wrote:

>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.

Oops. As these terms are used, it is commonly considered that elementary 
geometry is Tarski's theory of real closed fields (involving 
inequalities), where Collins' cylindrical algebraic decomposition 
method is the best so far. If all you care about are equalities, 
then Groebner bases will do.


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