基于质点法的构造型仿射几何定理机器证明.pdf

《基于质点法的构造型仿射几何定理机器证明.pdf》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、？．？一一４＼．’－＇户‘：：．Ｉ．巧告■＇＇？．下；．‘‘＾；為繁，．．．．？＇．Ｖ一Ｉ’：．．．＾．’．＞０１６５－：巧码：１分类号：请／学校代＇２０１２１１０００７４日巧统：：苦学号■和■－－？－違拿師範乂學藝語势硕±学位论义一．、：二ｉ心；隱無雜權謹：？？、…．．Ｖ蜡；；辖批巧巧：：．Ｖ奇靖．托？，巧；，，與姑基于质点法的构造型仿射几何定理机器证明＇＇＾泉；Ｖ—審款義；作者姓名＾

2、巧应用数学苟拳气学科、专业；—呼硏究方自动向：Ｍ＿＿江导师姓名：哼２０１５年３月＊■．＾Ｖ．二，；＾一＇－？一、．．一，二－‘…巧－＞，叫ＴＶ＇＇、’Ａ，Ａ餐义—一一？，■献，．学位论文独创性声明本人承诺：所呈交的学位论文是本人在导师指导下所取得的研究成巧。论文中除特别加标注和致谢的地方外，不包含他人和其他机构已经撰写或发表过的研巧成果，其他同志的研究成果对本人的启巧和所提供的帮助，均已在论文中做了明确的声明并表示谢意。学位论文作者签名：細

3、ｈ学位论文版权的使用授权书本学位论文作者完全了解迁宁师范大学有关保留、使用学位论文的规定，及学校鲁权保留并向国家有关部口或机构送交复印件或磁盘，允许论文被查和借。阅本文授权阅迁，宁师范大学可＾＾＾将学位论文入有关数据库的全部或部分内容编，可并进巧检索＾采＾用影、缩印印或扫描等制手段保存、汇编学位论文复，并且本人电子文档的内容和纸质论相一。文的内容致保密的学位论文在解密后使用本授权。书＾策續学位论文：敵作者签名指导教师签：名签名曰期：年月扫皆诚分类号：学校代码：10165密级：学号：2

4、01211000745硕士学位论文基于质点法的构造型仿射几何定理机器证明苏贺靓作者姓名：学科、专业：应用数学自动推理研究方向：江建国导师姓名：2015年3月辽宁师范大学硕士学位论文摘要几何定理的机器证明是自动推理领域的热门课题之一，尤其是近些年来，研究者在研究几何定理机器证明方面取得了丰硕的成果。吴文俊先生在1997年提出了“吴法”，几何定理机器证明的研究因而取得了重大突破。通常，几何定理机器证明方法可分为代数法，人工智能法和几何不变量法三大类。代数法的优点是证明效率高，缺点是可读性差；人工智能法虽然可读性好但不完备、效率低；

5、几何不变量法的可读性介于代数法和人工智能法之间，其证明效率与代数法也在伯仲之间。质点几何使用了比几何不变量更抽象的对象——质点，作为基本几何元素。莫绍揆先生在《质点几何学》一书中系统地阐述了质点几何的方法和理论。质点几何支持对点直接进行线性运算，在处理仿射几何问题时较为方便，为发展出一种效率更高、可读性更好的几何定理机器证明方法提供了可操作的依据。质点法是一种利用质点几何的基本原理和基本性质来证明构造型几何定理的完备性算法，具有运行效率高、可读性好、易于实现等优点。本文针对质点法生成的目标质点关系式的过程不简明，缺少明显的几何

6、意义的问题，提出了一种具有较高可读性算法的几何定理证明器MPP。为了进一步提高质点法的可读性和证明能力，具体提出了两大改进：一个是直接使用消点公式来推导目标质点关系式，另一个是利用待定系数法来统一地判定结论质点等式的正确性。基于改进后的质点法设计了该款几何定理证明器，并采用Matlab语言实现了该证明器。由于可以对点直接进行运算，证明器MPP的消点过程比原有质点法简明,具有更加明显的几何意义。在计算机上采用Matlab语言作了10个构造型仿射几何定理的运行实验，实验结果表明该证明器具有较高的运算效率。关键词：质点几何；证明器；

7、消点法；机器证明；自动推理-I-基于质点法的构造型仿射几何定理机器证明MachineProofsforAffineGeometricTheoremsofConstructiveTypeBasedonMassPointMethodAbstractGeometrictheoremprovingisahottopicinthefieldofautomatedreasoning,Researchershavemadegreatachievementsinthestudyofgeometrytheoremprovingaspectinr

8、ecentyears.SinceWu’smethodpublishedin1977,theresearchesandpractisesforautomatedprovingofgeometrytheoremshavebeenachievedmanybreakthroughs.