STR+VE Distribution Proposal

STR VE 分配方案

• 批准号: 9101980
• 负责人: Woodrow Bledsoe
• 金额: $ 2.91万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1991
• 资助国家: 美国
• 起止时间: 1991-05-01 至 1992-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9101980&HistoricalAwards=false
• 关键词: STR+VE; Distribution; Proposal

The goal of this software capitalization project is the development and distribution of a "release" quality version of STR+VE, a theorem prover for the first-order predicate calculus with inequality. This prover employs the Shielding Term Removal and Variable Elimination strategy with its emphasis on "larger steps". It is a fully automatic prover which has proved several important results in analysis, for example, the theorem that the sum of continuous functions is continuous.

这个软件资本化项目的目标是开发和分发STR+VE的“发布”质量版本，STR+VE是一阶谓词演算的一个定理证明器。该证明器采用了屏蔽项去除和变量消除策略，强调“较大的步数”。它是一个全自动证明器，已经证明了分析中的几个重要结果，例如连续函数和是连续的定理。