计算机应用
計算機應用
계산궤응용
COMPUTER APPLICATION
2014年
7期
2080-2084
,共5页
几何定理机器证明%确定性算法%概率性算法%构造性几何%变元次数上界
幾何定理機器證明%確定性算法%概率性算法%構造性幾何%變元次數上界
궤하정리궤기증명%학정성산법%개솔성산법%구조성궤하%변원차수상계
mechanical geometry theorem proving%deterministic algorithm%probabilistic algorithm%constructive geometry%upper bound of the degree of variable
将几何定理机器证明的研究方法概括为确定性算法与概率性算法两大类,针对已有的确定性算法和概率性算法的证明速率偏低或占用内存过大等问题,提出一种改进的概率性算法.主要是在改进对多项式中独立变元次数的上界估计的算法的基础上,结合Schwartz-Zippel定理和统计学理论,通过随机检验若干实例来证明几何定理,并能控制证明结果不真的概率在给定的小范围内.通过改进的概率性算法,成功在2秒内证明出代数法难以证明的五圆定理.最后的多组对比实验进一步表明,改进的概率性算法具有明显高效性.
將幾何定理機器證明的研究方法概括為確定性算法與概率性算法兩大類,針對已有的確定性算法和概率性算法的證明速率偏低或佔用內存過大等問題,提齣一種改進的概率性算法.主要是在改進對多項式中獨立變元次數的上界估計的算法的基礎上,結閤Schwartz-Zippel定理和統計學理論,通過隨機檢驗若榦實例來證明幾何定理,併能控製證明結果不真的概率在給定的小範圍內.通過改進的概率性算法,成功在2秒內證明齣代數法難以證明的五圓定理.最後的多組對比實驗進一步錶明,改進的概率性算法具有明顯高效性.
장궤하정리궤기증명적연구방법개괄위학정성산법여개솔성산법량대류,침대이유적학정성산법화개솔성산법적증명속솔편저혹점용내존과대등문제,제출일충개진적개솔성산법.주요시재개진대다항식중독립변원차수적상계고계적산법적기출상,결합Schwartz-Zippel정리화통계학이론,통과수궤검험약간실례래증명궤하정리,병능공제증명결과불진적개솔재급정적소범위내.통과개진적개솔성산법,성공재2초내증명출대수법난이증명적오원정리.최후적다조대비실험진일보표명,개진적개솔성산법구유명현고효성.