Analytics - An experiment in combining theorem proving and symbolic computation

被引：19

作者：

Bauer, A

Clarke, E

Zhao, XD

机构：

[1] Carnegie Mellon Univ, Sch Comp Sci, Pittsburgh, PA 15213 USA

[2] Intel Corp, Hillsboro, OR 97124 USA

来源：

JOURNAL OF AUTOMATED REASONING | 1998年 / 21卷 / 03期

基金：

美国国家科学基金会;

关键词：

computer algebra; Analytica; symbolic computation; Mathematica; theorem proving;

D O I：

10.1023/A:1006079212546

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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 Bernstein approximation theorem.

引用

页码：295 / 325

页数：31