## 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).