Accession Number : ADA258656


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


Descriptive Note : Research rept.


Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE


Personal Author(s) : Clarke, Edmund ; Zhao, Xudong


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a258656.pdf


Report Date : Oct 1992


Pagination or Media Count : 22


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. In this paper 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 examples including the basic properties of the stereographic projection and a series of three lemmas that lead to a proof of Weierstrass's example of a continuous nowhere differentiable function. Each of the lemmas in the latter example is proved completely automatically.


Descriptors :   *THEOREMS , *SYMBOLIC PROGRAMMING , FUNCTIONS , COMPUTATIONS , ENVIRONMENTS , STRUCTURES , DIVISION , GUARANTEES , ERRORS , LANGUAGE , AUTOMATIC


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE