SGARP中全角法的实现-论文.pdf

《SGARP中全角法的实现-论文.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、2014年6月广西师范学院学报：自然科学版Jun．2O14第31卷第2期JournalofGuangxiTeachersEducationUniversity：NaturalScienceEditionVo1．3lNo．2文章编号：1002—8743(2014)02—0033-04SGARP中全角法的实现张传军，郑焕。，邹宇(1．贵州省教育科学院，贵州贵阳550001；2．广州大学计算机科学与教育软件学院，广东广州51O006)摘要：在可持续发展的几何自动推理平台SGARP中，通过添加全角法相关的对象、谓词

2、和定理，在SGARP中成功实现了全角法．添加了全角法的SGARP测试证明了i00个几何定理．关键词：可持续发展的几何自动推理平台SGARP；全角法；西姆松定理中图分类号：TP181文献标识码：A1引言几何定理机器证明一直是近五十多年来国内外学者研究的热门课题之一，很多国家研制出了各种几何定理证明器，各有特色．可参见文献E1~9；．但这些软件都有一个共同的遗憾，就是几何定理证明器已经添加好了对象、规则和定理，不允许用户修改或者添加．直到文献[1O]提出了可由用户持续发展的几何自动推理平台sGARP，用户可以修

3、改和添加几何自动推理平台上的对象、规则和定理．本文在SGARP中通过添加全角的相关对象、谓词和定理实现了用全角法证明很多定理．2全角法的实现定义1E¨]同一平面上的两条直线AB和MN构成的有序对，叫做一个全角，记作．周、高、张等人[1幻引入了全角来替代传统角，将全角选作几何不变量，并将“消点”的思想推广到“消线”，提出了一个基于全角的消点法，即全角法L1．本文在SGARP中通过添加全角的相关对象、谓词和定理实现了用全角法证明很多定理．添加的对象有：FullAngle(ABCD)，表示全角

4、D>．添加的谓词有：Equal1一FullAngle(F(GHCBCB)，表示全角一；谓词Measure-FullAngle(ABCDd)，表示全角=d；谓词AddTwoLine—FullAngle(FGGHCBEBEBBH)表示一+；谓词LineIntersecti0n(FFEHE)表示F是直线阳和直线HE的交点；谓词Cocircle(DFEG)表示四点D、E、F、G共圆；谓词Collinear(DFC)表示三点D、F、C共线；谓词P

5、erpendicular(EFDC)表示直线EF垂直于直线DC．添加的定理有：自反律Self-FullAngle，对称律Sym-FullAngle，传递律Trans-FullAngle，平角律Parallel—FullAngle，直角律PerpendRv—FullAngle，过渡律Transition-FullAngle，代换律Substitution，圆周角定理CircumFuttAnglel，CircumFullAngle2等等一系列与全角性质和结论相关的对象、谓词和定理．实现了用全角法证明很多定理．收

6、稿日期：2014—05-13*基金项目：国家自然科学基金联合基金(U12O1252)国家自然科学基金(11326212)；广州市教育局科技项目(2o12Ao19)；贵州省教育科学规划重点项目(2o13Ao68)作者简介：张传军(1979一)，男，吉林敦化人，讲师，博士，主要研究方向：几何自动推理，半群．·36·广西师范学院学报：自然科学版第31卷[4]GCLChomepage．http：／／www．matf．bg．ac．rs／～janicic／／gc1c／．[53CAFERRAR。PELTIERN，PUIT

7、GF．EmphasizingHumanTechniquesinAutomatedGeometryTheoremPro—ving：APracticalRealization[C]／／RICHTER-GEBERTJ，WANGD．AutomatedDeductioninGeometry，LNAI2061．Berlin：springer-Verlag，2001：268-305．[6]MATSUDAN，VANLEHNK．AdvancedGeometryTutor：Anintelligenttutorthatteach

8、esproobwritingwithconstruction[C]／／Proceedingsofthe12thInternationalConferenceonArtificialIntelligenceinEducation．Kanaza—wa，2005：443-450．[7]WILSONS，FLEURIoTJD．CombiningDynamicGeometry，AutomatedGeometryTheorem