摘要
将几何定理机器证明的研究方法概括为确定性算法与概率性算法两大类,针对已有的确定性算法和概率性算法的证明速率偏低或占用内存过大等问题,提出一种改进的概率性算法。主要是在改进对多项式中独立变元次数的上界估计的算法的基础上,结合Schwartz-Zippel定理和统计学理论,通过随机检验若干实例来证明几何定理,并能控制证明结果不真的概率在给定的小范围内。通过改进的概率性算法,成功在2秒内证明出代数法难以证明的五圆定理。最后的多组对比实验进一步表明,改进的概率性算法具有明显高效性。
The research methods of mechanical geometry theorem proving were summed up into two categories, deterministic algorithms and probabilistic algorithms, and then an improved probabilistic algorithm was proposed to overcome the drawbacks such as poor efficiency or memory consumption in the existing methods. That was, the upper bounds of the degrees of variables in the pseudo-remainder were estimated by adopting an improved algorithm, and then on the basis of combining Schwartz-Zippel theorem and statistical theory, a geometric theorem could be proved by checking several random instances, the probability of error result could also be calculated and controlled within any given small range. Through the improved probabilistic algorithm, the Five Circles Theorem had already been proved successfully within two seconds which is quite difficult to be proved by existing algebra methods for its high complexity. Comparative experiment results also show that the improved probabilistic algorithm is high efficient.
出处
《计算机应用》
CSCD
北大核心
2014年第7期2080-2084,共5页
journal of Computer Applications
基金
教育部博士点基金资助项目(20110076110010)
关键词
几何定理机器证明
确定性算法
概率性算法
构造性几何
变元次数上界
mechanical geometry theorem proving
deterministic algorithm
probabilistic algorithm
constructivegeometry
upper bound of the degree of variable