The Mathematica Journal


About the Journal
Current Issue
Editorial Policy
Back Issues
Contact Information


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.