教育信息化是实现教育现代化的重要步骤,是教育现代化的重要内容和主要标志。数学既是一门基础学科,又是一门思维学科,其教学对于培养学生的思维能力、运算能力、想象能力、实践能力和创造能力起到非常重要的作用。数学证明是数学教学的一项重要内容,在训练及考核中具有其它方式方法不可替代的作用。如何在数学证明的教学中运用现代信息技术,实现对数学证明的形式化分析和验证,越来越多地引起人们的关注。在中学数学教学中,初等代数是学习平面几何、立体几何、三角函数、解析几何以及微积分等内容的基础,如何由计算机自动完成对主观试题的答案,尤其是初等代数证明题答案的验证也成为一个在理论上和实践中都有待解决的问题,有着广泛的应用前景。本文主要针对作为代数证明题答案的数学证明展开研究。在分析数学证明语言有关特性的基础上,提出一种表达数学证明的部分语句系统；通过基于话语表现理论的动态语义分析方法得到数学证明的形式语义；然后在机器定理证明系统中对它进行自动验证,从而得出原始证明是否正确的结论。研究涉及到语言学、逻辑学、计算科学和数学等多个学科的有关内容,具体包括：(1)数学证明语言特性分析数学证明语言是我们在解答证明题,书写答案时所使用的语言,它具有半形式化的特性,即在自然语言中还加上了数学公式。本文从数学和语言两个方面分析了它的基本特点。(2)数学证明部分语句系统句法分析是自然语言处理的一个难点。从蒙太格著名的PTQ开始,对形式语义学的研究往往通过构造部分语句系统来展开,如广义量词理论、情境语义学、话语表现理论、类型逻辑语法等。本文构造了一个表达数学证明的部分语句系统,可以满足数学证明的基本要求。(3)数学证明形式语义分析话语表现理论是最早提出来的动态语义理论。它把传统语义学的分析对象由单个句子扩展到句子系列,体现出代词与其先行词之间的照应关系。本文对话语表现理论的构造规则和话语表现结构进行了扩展,使其能够满足分析数学证明的需要。(4)数学证明的自动化验证机器定理证明是一个利用机器证明数学定理的人工智能研究领域。本文研究把数学证明的DRS转化为Isabelle/HOL的形式证明的方法,以及在Isabelle/HOL中对它进行验证的自动化策略,并对基于策略的计算进行了分析。