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.
