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
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