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