导　　师： 张景中;李传中

学科专业： D0102

授予学位： 硕士

作　　者： ;

机构地区： 广州大学

摘　　要： 从50年代tarski发表的《初等代数与初等几何的判定问题》<'[25]>开始,到70年代的吴法<'[4,5]>,90年代的消点法<'[8,10]>,几何定理机器证明的研究经历了几个阶段的发展.计算机技术的发展及可读机器证明的出现<'[3,4]>,使这个方向的研究成果进入了实用阶段.以张景中院士为领导的小组在此基础上开发了一系列的智能教育软件<'[10]>.得到广大中小学教师,学生的欢迎.这些软件最突出的一个特点就是自动推理.要让计算机能够自动进行推理.首先要"教会"计算机推理的方法,计算机"掌握"了方法后,才能进行推理.因此,"教会"计算机推理方法是首要的.现行的推理软件都是采用了前推搜索的推理模式.从题目的已知条件出发,利用规则进行推理直至推出所需要的结论.在数学证明方法上属于直接证明方法.这种方法只能证明一些肯定性的命题.但对于一些否定性,唯一性的命题采用直接证法不易证明,这就需要利用数学证明中的间接证明方法来证明.间接证明方法中比较常见的一种方法是反证法.尽管几何定理机器证明的研究在七十年代已经取得突破,可读证明的实现也近十年了.但自动推理在反证法方面还存在很大的不足.除了在《平面几何》<'[22]>中见到有间接证法中的同一法外,其他的教育软件中很少有实现反证法的.该文的工作就是向这个方向努力的一个尝试,把数学证明中的反证法与机器证明中的前推搜索法相结合.使计算机在自动推理方面能够更加完善.该文共分为四章:第一章,简要介绍自动推理的历史和发展,阐述该文要解决的问题.第二章,介绍该文的工作原理及实现技术.第三章,给出作者今后的工作方向.第四章,给出该系统证明的一些例题.

关 键 词： 规则 自动推理 前推搜索 语句 矛盾

分 类 号： [G436 G633.6]

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