[FOM] Automatic theorem proving in trigonometry and synthetic geometry
Mitchell Harris
harris at tcs.inf.tu-dresden.de
Thu Jul 22 03:57:07 EDT 2004
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
More information about the FOM
mailing list