几何定理机器证明系统的开发与研究

《几何定理机器证明系统的开发与研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、北京化工大学硕士学位论文几何定理机器证明系统的开发与研究姓名：尤枫申请学位级别：硕士专业：计算机应用技术指导教师：朱望规2003.5.27北京化工大学硕士生学位论文几何定理机器证明系统的开发与研究摘要【通常，几何定理的证明是依据公理系统，按一定的逻辑规则演绎＼地进行。对于每一个定理，其证明的方法都是不同的，一种方法只适用于一个定理，没有通用的证明方法或指导思想适合于所有的定理哪怕是某一类定理，证明方法不能触类旁通，只能凭借经验和严密的逻辑判断能力来进行。随着20世纪70年代吴文俊先生关于数学机械化方法的创立，使得机械化证明和计算在数学的许多领域才成为现

2、实。这一被称为吴方法的数学机械化方法，特别在几何定理机械化证明中得到了很好的应用。这是基于构造性的代数几何理论的一种证明方法，使得证明可以沿着一条有规律的刻板的道路进行，为几何定理的证明开辟了新的途径。0、／本文围绕数学机械化的吴方法展开了对初等几何机械化证明的探讨和研究，主要内容包括：(1)以Maple和Matlab系统为支撑开发了运用该方法证明定理的软件系统。(2)对大量的定理进行了实验性证明。(3)对采用该方法进行证明时存在的问题进行了研究。关键词：吴方法，、几何定理i机器证明，、特征列北京化工大学硕士生学位论文RESEARCHANDDEVELo

3、PMENToFMACHINEPRoVINGSYSTEMoNGEoMETRYTHEoREMAbstractGenerally,theproving0fgeometrytheoremisbasedontheaxiomsystem，andisdeductedaccordingtocertainlogicrules．Differenttheoremhasdifferentprovingmethod，andnocommonwaysorideascanbeusedforalltheoremsorevenforacertainclass．Soitcall’tbeco

4、mprehendedbyanalogyforproving，andCanonlybeputintorealitybyexperienceandpreciselogicaljudgmentcapability．WiththefoundationofMr．Wuwenjun’Smethodofmathematicalmechanization，themechanicalprovingandcalculatingareputintorealityinmanyfieldsofmath．Thismechanicalmethod，calledWu’Smethod，i

5、sespeciallywellappliedintotheMechanicalGeometryTheoremProving，whichisaprovingmethodbasedonthestructuralgeometryalgebratheorem，andbreaksanewpathfortheprovingofgeometrytheorem．ThispapermainlydiscussesthemechanicalprovingofelementarygeometrybasedontheWu’Smethod，including：(1)develop

6、ingasoftwaresystemusingthismethodtoprovetheorembasedontheMapleandMatlab．(2)validatingthesystemusinglargeamountoftheorems．(3)makingdeepresearchesonthekeyproblemsduringtheprocessofIl北京化工大学硕士生学位论文provingKeywords：Wu’smethod，geometrytheorem,machineproving，CharacteristicSetsIII北京化工大学学

7、位论文原创性声明y50105-7本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究工作所取得的成果。除文中已经注明引用的内容外，本论文不含任何其他个人或集体已经发表或撰写过的作品成果。对本文的研究做出重要贡献的个人和集体，均已在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。学位论文作者签名：罐，栩)即≥年f月27日北京化工大学硕士研究生学位论文1．1机器证明概述第一章文献综述数学是研究数量关系和形体性质的科学，它具有表达精确，论证严谨的特点。“数”与“形”在自然界中是无处不在的，因此可以肯定地说数学是自然科学的基石，也是

8、高新技术的理论基础，是联系科学与技术的纽带。数学机械化研究目前已成为西方发达国家积极研究的前沿