Wolfram Library Archive

Courseware Demos MathSource Technical Notes
All Collections Articles Books Conference Proceedings

Analytica: A Theorem Prover for Mathematica

Edmund Clarke
Xudong Zhao
Journal / Anthology

The Mathematica Journal
Year: 1993
Volume: 3
Issue: 1
Page range: 56-71

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

*Applied Mathematics > Computer Science
*Mathematics > Foundations of Mathematics > Logic
Related items

*Analytica--A Theorem Prover in Mathematica   [in Articles]