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

A GEOMETRY PROVER BASED ON COMBINED PROBABILISTIC CHECKING MODEL

作　　者：陈明雁[1] 曾振柄[1] 

机构地区：[1]上海大学数学系,上海200444

出　　处：《系统科学与数学》2015年第6期627-644,共18页Journal of Systems Science and Mathematical Sciences

基　　金：教育部博士点基金(20110076110010);国家自然科学基金(11471209)资助课题

摘　　要：以概率性算法代替传统的确定性算法可快速证明复杂度很高的几何定理,可大幅度提高证明效率.对估算多项式中独立变元次数上界的算法进行了改进,并提出三种统计总体的采集标准,分析两种不同的实例检验方法,结合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.

关 键 词：几何定理机器证明 概率性算法 变元次数的上界 统计总体采集标准 概率检测组合模型 

分 类 号：O213[理学—概率论与数理统计]