Analytica — An Experiment in Combining Theorem Proving and Symbolic Computation

• 01 August 1997
• Andrej Bauer
• Publications

with Edmund Clarke and Xudong Zhao.

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 deduce 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 non-trivial theorems. In this paper, we show how it can prove a series of lemmas that lead to Bernstein approximation theorem.

Published in: Journal of Automated Reasoning, Vol. 21, no.3 (1998) 295-325

Download: analytica.pdf, analytica.ps.gz

Source code: analytica.tar.gz contains the source code for Analytica. It works under Mathematica 2.2.2. I do not plan to port it to a newer version of Mathematics. If you do that, please let me know.