导　　师： 张景中;李传中

学科专业： D0102

授予学位： 硕士

作　　者： ;

机构地区： 广州大学

摘　　要： 几何定理机器证明的研究在最近20年来取得了一系列令人瞩目的成果,特别是计算机自动推理可读证明的突破,使几何定理机器证明的研究成果进入实用阶段,应用于中学教学,成为计算机辅助教学的有力工具.其中以"z+z智能教育平台"系列的《平面几何》、《解析几何》等为代表的智能教育软件在同类软件中独树一帜.该系列的特色之一自动推理,能在一个合理的时间内,对大多数的几何命题给出符合人们阅读习惯的传统证明过程,受到了广大中小学教师和学生的欢迎,开辟了几何定理机器证明新的应用领域.让计算机解几何题,一个重要的问题是提高推理的效率.如何在系统中合理的组织几何信息的数据结构,是提高效率的一个关键因素.该文旨在说明几何信息在推理时压缩的实现,并介绍了压缩信息的展开与提取.另一方面,表达式的推理不同于一般信息的推理,它没有固定的格式,该文提出一种表达式推理的方法,是向这个方向的一个尝试,能对一般的结论为表达式的例题给出可读的证明过程.该文分五章:第一章是绪论.简要介绍了计算机自动推理的历史和发展,自动推理在当前教育软件方面的应用,并说明了该文的工作.第二章介绍了几何定理可读证明的思想.第三章以相等角为例,说明了几何信息的压缩与展开在自动推理中的实现.第四章分析并处理了结论为表达式的命题在自动推理中的实现.第五章是结论部分,给出了该文工作的意义及今后的工作方向.最后以附录的形式列出了与该文内容相关的几何例子.

关 键 词： 自动推理 可读证明 信息的压缩 表达式

分 类 号： [G436 G633.63]

领　　域： [文化科学] [文化科学] [文化科学]