改进的几何定理机器证明的概率性算法-论文.pdf

《改进的几何定理机器证明的概率性算法-论文.pdf》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。

1、JournalofComputerApplicationsISSN1001—90812014．．07．10计算机应用，2014，34(7)：2080—2084CODENJYIIDUhttp：／／www．joca．ca文章编号：1001—9081(2014)07—2080—05doi：10．11772／j．issn．1001—9081．2014．07．2080改进的几何定理机器证明的概率性算法陈明雁’，曾振柄(1．上海高可信计算重点实验室(华东师范大学)，上海200062；2．上海大学数学系，上海200444)($通信作者电子邮箱mychen@ecnu．cn)摘要：将几何定

2、理机器证明的研究方法概括为确定性算法与概率性算法两大类，针对已有的确定性算法和概率性算法的证明速率偏低或占用内存过大等问题，提出一种改进的概率性算法。主要是在改进对多项式中独立变元次数的上界估计的算法的基础上，结合Schwartz·Zippel定理和统计学理论，通过随机检验若干实例来证明几何定理，并能控制证明结果不真的概率在给定的小范围内。通过改进的概率性算法，成功在2秒内证明出代数法难以证明的五圆定理。最后的多组对比实验进一步表明，改进的概率性算法具有明显高效性。关键词：几何定理机器证明；确定性算法；概率性算法；构造性几何；变元次数上界中图分类号：TP181文献标志码：

3、AImprovedprobabilisticalgorithmofmechanicalgeometrytheoremprovingCHENMingyan，ZENGZhenbing(1．ShanghaiKeyLaboratoryofTrustworthyComputing(EastChinaNormalUniversity)，Shanghai200062，China；2．DepartmentofMathematics，ShanghaiUnive~i@,Shanghai200444，China)Abstract：Theresearchmethodsofmechanicalge

4、ometrytheoremprovingweresummedupintotwocategories，deterministicalgorithmsandprobabilisticalgorithms，andthenanimprovedprobabilisticalgorithmwasproposedtoovercomethedrawbackssuchaspooreficiencyormemoryconsumptionintheexistingmethods．ThatWas．theupperboundsofthedegreesofvariablesinthepseudo—r

5、emainderwereestimatedbyadoptinganimprovedalgorithm，andthenonthebasisofcombiningSchwartz-Zippeltheoremandstatisticaltheory，ageometrictheoremcouldbeprovedbycheckingseveralrandominstances，theprobabilityoferrorresultcouldalsobecalculatedandcontrolledwithinanygivensmallrange．Throughtheimproved

6、probabilisticalgorithm，theFiveCirclesTheoremhadalreadybeenprovedsuccessfulywithintwosecondswhichisquitedificulttobeprovedbyexistingalgebramethodsforitshighcomplexity．ComparativeexperimentresultsalsoshowthattheimprovedprobabilisticalgorithmishJghefficient．Keywords：mechanicalgeometrytheorem

7、proving；deterministicalgorithm；probabilisticalgorithm；constructivegeometry；upperboundofthedegreeofvariable发展了一种这种例证法的单例实验法。继洪加威的例证法，0引言1989年，张景中等发展的数值并行法以数值计算和并行处理几何定理机器证明是指通过机器自动地证明几何定理，方式有效地减少了内存消耗和证明时间，成为第一个具有实是数学机械化的重要部分。常用的方法可分为三种：代数法、践性意义的数值方法J。然而，数值并行法对需要验证实向