 |
|
|
|
|
 |
|
|
Analytica--An Experiment in Combining Theorem Proving and Symbolic Computation
|
|
|
|
|
|
|
|
|
|
|
|
| Journal of Automated Reasoning |
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
For the newest resources, visit Wolfram Repositories and Archives »
