RUI: Logic and Computation: Automating Proofs in Calculus and Analysis in Teacher Preparation

目前有能够表示数学证明的大型计算机程序（如NuPrl）和能够进行符号计算的大型计算机程序（如Macsyma），以及许多试图寻找证明的定理证明程序。但这三种能力在同一个系统中根本不存在。在这个项目中，将建立一个将符号计算和数学证明表示顺利集成的单一系统，并辅以证明查找算法。一个原型版本已经能够自动生成f(x) = x^3的连续性的ε - δ证明。要建立的系统将能够生成许多其他的证明和其他更复杂的分析证明。＊＊＊

At present there are large computer programs capable of representing mathematical proofs (such as NuPrl) and large computer programs capable of symbolic computation (such as Macsyma), and many theorem-proving programs that try to find proofs. But these three capabilities are nowhere present in the same system. In this project, a single system smoothly integrating symbolic computation and representation of mathematical proofs will be built, and supplemented with proof-finding algorithms. A prototype version has already been able to generate automatically an epsilon-delta proof of the continuity of f(x) = x^3. The system to be built will be able to generate many other epsilon-delta proofs and other more complicated proofs in analysis. ***