Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation
Abstract
Analytica is an automatic theorem prover for theorems in elementary analysis. The prover is written in mathematica language and runs in the mathematica environment. 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. The theorem prover 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. In this paper we describe the structure of Analytica and explain the main techniques that it uses to construct proofs. Analytica has been able to prove several non-trivial examples including the basic properties of the stereographic projection and a series of three lemmas that lead to a proof of Weierstrass's example of a continuous nowhere differentiable function. Each of the lemmas in the latter example is proved completely automatically.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 1992
- Accession Number
- ADA258656
Entities
People
- Edmund M. Clarke
- Xudong Zhao
Organizations
- Carnegie Mellon University