Automated Generation of Readable Proofs for a Class of Limits of Sequences and Functions*

Jing Ruan** and Zhengyi Lu
Department of Mathematics
Wenzhou University
Wenzhou 325003, China
**Wenzhou Vocational and Technical College
Wenzhou 325003, China

Abstract. Computer algebra systems have been widely used for symbolic and numeric computation. It plays a significant role in the computation of differentials, integrals, limits, etc.

In general, the proofs for limits of sequences and functions by definition depend on our experience. In this talk, we present two algorithms for generating readable proofs automatically for a class of limits of sequences and functions by definition under a computer algebra system. For every given epsilon>0, how to find a corresponding positive number N (delta or M) for the proofs for limits of sequences (functions) is a key point in our proofs. Using the command limsp (limfp) in the symbolic computation software Maple, readable proofs of the limits will be obtained by the proposed algorithms. Seven examples will be presented to illustrate the implementation of the programs.

*Partially supported by the National Natural Science Foundation of China (Grant no. 10371090) and a National Key Basic Research Project of China (Grant no. 2004CB318000).