STR+VE Distribution Proposal

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

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.