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