Analytica: A Theorem Prover for Mathematica
Volume 3, Issue 1
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.