Wolfram Library Archive

Courseware Demos MathSource Technical Notes
All Collections Articles Books Conference Proceedings

Analytica--An Experiment in Combining Theorem Proving and Symbolic Computation

A. Bauer
Edmund Clarke
Xudong Zhao
Journal / Anthology

Journal of Automated Reasoning
Year: 1998
Volume: 21
Page range: 295-325

Analytica is an automatic theorem prover for theorems in elementary analysis. The prover is written in the 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 deduce the correctness of certain simplification steps that would otherwise not be performed. We describe the structure of Analytica and explain the main techniques that it uses to construct proofs. Analytica has been able to prove several nontrivial theorems. In this paper, we show how it can prove a series of lemmas that lead to the Berstein approximation theorem.

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