The Mathematica Journal

Search

About the Journal
Current Issue
Editorial Policy
Submissions
Back Issues
Contact Information

index.html

Analytica: A Theorem Prover for Mathematica

Volume 3, Issue 1
Winter 1993
Edmund Clarke and Xudong Zhao,  Carnegie Mellon University
 

Analytica is an automatic theorem prover written in Mathematica for theorems in elementary analysis. The goal of the project is to use a powerful symbolic computation system to prove theorems that are beyond the scope of previous automatic theorem provers. Analytica is also able to guarantee the correctness of certain steps that are made by the symbolic computation system and therefore prevent common errors like division by a symbolic expression that could be zero. We describe the structure of Analytica and explain the main techniques it uses to construct proofs. We illustrate Analytica's power with several examples including the basic properties of the stereographic projection and a series of three lemmas, each proved completely automatically, that lead to a proof of Weierstrass's example of a continuous nowhere-differentiable function.

     
About Mathematica 
© Wolfram Media, Inc. All rights reserved.