反证法在自动推理系统中的研究与实现

《反证法在自动推理系统中的研究与实现》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、广州大学硕士学位论文反证法在自动推理系统中的研究与实现姓名：李晓霞申请学位级别：硕士专业：课程与教学论指导教师：张景中;李传中20040501摘要从50年代Tarski发表的《初等代数与初等几何的判定问题》【251开始，到70年代的吴法14．5】，90年代的消点法【8，】01，几何定理机器证明的研究经历了几个阶段的发展。计算机技术的发展及可读机器证明的出现[3，41，使这个方向的研究成果进入了实用阶段。以张景中院士为领导的小组在此基础上开发了一系列的智能教育软件【”】。得到广大中小学教师，学生的欢迎。这些软件最突出的一个特点就是自

2、动推理。要让计算机能够自动进行推理。首先要“教会”计算机推理的方法，计算机“掌握”了方法后，才能进行推理。因此，“教会”计算机推理方法是首要的。现行的推理软件都是采用了前推搜索的推理模式。从题目的己知条件出发，利用规则进行推理直至推出所需要的结论。在数学证明方法上属于直接证明方法。这种方法只能证明一些肯定性的命题。但对于一些否定性，唯一性的命题采用直接证法不易证明，这就需要利用数学证明中的间接证明方法来证明。间接证明方法中比较常见的一种方法是反证法。尽管几何定理机器证明的研究在七十年代已经取得突破，可读证明的实现也近十年了。但自动

3、推理在反证法方面还存在很大的不足。除了在《平面几何》【22l中见到有间接证法中的同一法外，其他的教育软件中很少有实现反证法的。本文的工作就是向这个方向努力的一个尝试，把数学证明中的反证法与机器证明中的前推搜索法相结合。使计算机在自动推理方面能够更加完善。本文共分为四章：第一章，简要介绍自动推理的历史和发展，阐述本文要解决的问题。第二章，介绍本文的工作原理及实现技术。第三章，给出作者今后的工作方向。第四章，给出本系统证明的～些例题。V一J丛幽型L———————————————一AbstractFromtlrsl(i，snotable

4、work‘‘ADecisionMethodforElementaryAlgebraandGeometry’’in1950stothe1970s’Wu’SMethodandthe1990s’PointsEliminationMethod．ThedevelopmentoftheresearchofAutomatedReasoninginGeometryhasexperiencedseveralsteps．AsthedevelopmentofcomputertechnologyandthediscoveryofReadableProof

5、sonmachineproofs，theresultsinthisfieldhavebeenputintouse．ThegroupwhichleadbyZhangJingzhonghavedevelopedaseriesofintelligenteducationalsoffwares，thesoftwarewerewelcomedastheyfirstpublished，Themostoutstandingcharacteristicofthesoftwareistheautomaticreasoning．Letthecompu

6、terabletoCalTyonreasoningautomatically．Should”teach’’thereasoningmethodofthecomputerfirst，afterthecomputerhas”grasped”themethod，Couldcarryonreasoning．So，itisprimaryto”teach”thereasoningmethodofthecomputer．Atpresent,mostsoftwareusedForwardChain．Fromtheknownconditionsto

7、results．Whichisamethodofdirectlyproving，thismethodonlyprovesomeaffirmativepropositions，buttosomenegative，solitarypropositionsisverydifficulttoprove．Whichneedindirectlymethodtoprove．，Theproofbycontradictionisoftenusedinindirectlyproving．ThoughtheresearchofAutomatedReas

8、oninginGeometryhadgainedsucceedin1970’S，thereisalmosttenyearssincethediscoveryofreadableproof，buttheautomatedreasoningisshor