Analytica — An experiment in combining theorem proving and symbolic computation
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.
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.
KeywordsCurrent Context Sequent Calculus Induction Scheme High Order Logic Inference Phase
Unable to display preview. Download preview PDF.
- 2.B. C. Berndt. Ramanujan's Notebooks, Part I. Springer-Verlag, 1985.Google Scholar
- 3.W. W. Bledsoe. The ut natural deduction prover. Technical Report ATP-17B, Mathematical Dept., University of Texas at Austin, 1983.Google Scholar
- 4.W. W. Bledsoe. Some automatic proofs in analysis. In Automated Theorem Proving: After 25 Years. American Mathematical Society, 1984.Google Scholar
- 5.W. W. Bledsoe, P. Bruell, and R. E. Shostak. A prover for general inequalities. Technical Report ATP-40A, Mathematical Dept., University of Texas at Austin, 1979.Google Scholar
- 6.R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, 1979.Google Scholar
- 7.A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Technical report, Department of Artificial Intelligence, University of Edinburgh, 1988.Google Scholar
- 8.E. M. Clarke and X. Zhao. Analytica: A theorem prover for mathematica. The Journal of Mathematica, 3(1), 1993.Google Scholar
- 9.W. M. Farmer, J. D. Guttman, and F. J. Thayer. Imps: An interactive mathematical proof system. Technical report, The MITRE Corporation, 1990.Google Scholar
- 10.M. Fitting. First-order Logic and Automated Theorem Proving. Springer-Verlag, 1990.Google Scholar
- 11.J. H. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, 1986.Google Scholar
- 12.M. Gorden. Hol: A machine oriented formulation of higher order logic. Technical report, Computer Laboratory, University of Cambridge, 1985.Google Scholar
- 13.M. Gorden, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanised logic of computation, volume 131 of Lecture Notes in Computer Science. Springer-Verlag, 1979.Google Scholar
- 14.R. W. Gosper. Indefinite hypergeometric sums in macsyma. In Proceedings of the MACSYMA Users Conference, pages 237–252, 1977.Google Scholar
- 15.R. L. London and D. R. Musser. The application of a symbolic mathematical system to program verification. Technical report, USC Information Science Institute, 1975.Google Scholar
- 16.A. Quaife. Automated deduction in von neumann-bernays-godel set theory. Technical report, Dept. of Mathematics, Univ. of California at Berkeley, 1989.Google Scholar
- 17.E. Sacks. Hierarchical inequality reasoning. Technical report, MIT Laboratory for Computer Science, 1987.Google Scholar
- 18.P. Suppes and S. Takahashi. An interactive calculus theorem-prover for continuity properties. Journal of Symbolic Computation, 7:573–590, 1989.Google Scholar
- 19.S. Wolfram. Mathematica: A System for Doing Mathematics by Computer. Wolfram Research Inc., 1988.Google Scholar