Advertisement

Analytica — An experiment in combining theorem proving and symbolic computation

  • Andrej Bauer
  • Edmund Clarke
  • Xudong Zhao
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1138)

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.

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.

Keywords

Current Context Sequent Calculus Induction Scheme High Order Logic Inference Phase 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    P. B. Andrews. On connections and higher-order logic. Journal of Automated Reasoning, 5:257–291, 1989.CrossRefGoogle Scholar
  2. 2.
    B. C. Berndt. Ramanujan's Notebooks, Part I. Springer-Verlag, 1985.Google Scholar
  3. 3.
    W. W. Bledsoe. The ut natural deduction prover. Technical Report ATP-17B, Mathematical Dept., University of Texas at Austin, 1983.Google Scholar
  4. 4.
    W. W. Bledsoe. Some automatic proofs in analysis. In Automated Theorem Proving: After 25 Years. American Mathematical Society, 1984.Google Scholar
  5. 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. 6.
    R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, 1979.Google Scholar
  7. 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. 8.
    E. M. Clarke and X. Zhao. Analytica: A theorem prover for mathematica. The Journal of Mathematica, 3(1), 1993.Google Scholar
  9. 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. 10.
    M. Fitting. First-order Logic and Automated Theorem Proving. Springer-Verlag, 1990.Google Scholar
  11. 11.
    J. H. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, 1986.Google Scholar
  12. 12.
    M. Gorden. Hol: A machine oriented formulation of higher order logic. Technical report, Computer Laboratory, University of Cambridge, 1985.Google Scholar
  13. 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. 14.
    R. W. Gosper. Indefinite hypergeometric sums in macsyma. In Proceedings of the MACSYMA Users Conference, pages 237–252, 1977.Google Scholar
  15. 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. 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. 17.
    E. Sacks. Hierarchical inequality reasoning. Technical report, MIT Laboratory for Computer Science, 1987.Google Scholar
  18. 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. 19.
    S. Wolfram. Mathematica: A System for Doing Mathematics by Computer. Wolfram Research Inc., 1988.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Andrej Bauer
    • 1
  • Edmund Clarke
    • 1
  • Xudong Zhao
    • 1
  1. 1.School of Computer ScienceCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations