基于概率检测组合模型的几何定理证明器

A GEOMETRY PROVER BASED ON COMBINED PROBABILISTIC CHECKING MODEL

以概率性算法代替传统的确定性算法可快速证明复杂度很高的几何定理,可大幅度提高证明效率.对估算多项式中独立变元次数上界的算法进行了改进,并提出三种统计总体的采集标准,分析两种不同的实例检验方法,结合Schwartz-Zippel定理与统计推断理论,建立概率检测组合模型,并在此基础上采用Maple编程语言实现此快速的几何定理证明器——ProbProver.利用ProbProver证明器可在2秒内证明出代数法较难证明的Five Circles定理.最后给出的多组对比实验进一步表明ProbProver证明器具有明显高效性.

Using probabilistic algorithm instead of traditional deterministic algorithm in geometry theorem proving can prove high complexity theorems in a short time and thus to improve the efficiency of proof greatly.In this paper,we improve the algorithm of estimating the upper bounds about the degrees of variables in pseudoremainder polynomial,and then propose three selection criteria for statistical population and apply two checking methods for instances verification.By combining Schwartz-Zippel Theorem with statistical inference theory,we develop a geometry theorem prover based on combined probabilistic checking model in Maple platform.Our prover is preponderant for its high performance,and it has successfully proven Five Circles Theorem which has not yet been proven by existing algebraic methods.Comparative experiment results show that ProbProver is high efficiency.