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

RUI：逻辑与计算：微积分中的自动化证明和教师准备中的分析

• 批准号: 9528913
• 负责人: Michael Beeson
• 金额: $ 8.5万
• 依托单位: San Jose State University Foundation
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1996
• 资助国家: 美国
• 起止时间: 1996-07-01 至 1999-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9528913&HistoricalAwards=false
• 关键词: RUI; Logic; Computation; Automating; Proofs

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

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