An interactive calculus theorem-prover for continuityproperties
Patrick Suppes, Shuzo Takahashi · Journal of Symbolic Computation · 1989
The work reported concerns the development of an interactive theorem-prover for the foundations of the differential and integral calculus. The mam tools are a resolution theoremprover VERIFY, prewously developed for interactive proofs m set theory, and the symbolic computation program REDUCE. The use of REDUCE in a theorem-proving context IS described in detail. Sample proofs are given with data on computation time per step on an IBM-