改进的几何定理机器证明的概率性算法

doi:10.11772/j.issn.1001-9081.2014.07.2080

计算机应用 ›› 2014, Vol. 34 ›› Issue (7): 2080-2084.DOI: 10.11772/j.issn.1001-9081.2014.07.2080

改进的几何定理机器证明的概率性算法

陈明雁¹,曾振柄²

1. 上海高可信计算重点实验室(华东师范大学)，上海 200062
2. 上海大学数学系，上海 200444

收稿日期:2014-01-20 修回日期:2014-03-03 出版日期:2014-07-01 发布日期:2014-08-01
通讯作者: 陈明雁
作者简介:陈明雁(1987-)，女，广西贵港人，硕士研究生，主要研究方向：符号计算、自动推理；曾振柄(1963-)，男，甘肃皋兰人，教授，博士生导师，主要研究方向：符号计算、人工智能、自动推理。
基金资助:
教育部博士点基金资助项目

Improved probabilistic algorithm of mechanical geometry theorem proving

CHEN Mingyan¹,ZENG Zhenbing²

1. Shanghai Key Laboratory of Trustworthy Computing(East China Normal University), Shanghai 200062, China;
2. Department of Mathematics, Shanghai University, Shanghai 200444, China

Received:2014-01-20 Revised:2014-03-03 Online:2014-07-01 Published:2014-08-01
Contact: CHEN Mingyan

摘要/Abstract

摘要：

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

Abstract:

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.

中图分类号:

TP181

陈明雁曾振柄. 改进的几何定理机器证明的概率性算法[J]. 计算机应用, 2014, 34(7): 2080-2084.

CHEN Mingyan ZENG Zhenbing. Improved probabilistic algorithm of mechanical geometry theorem proving[J]. Journal of Computer Applications, 2014, 34(7): 2080-2084.

参考文献

［1］WU W. On the decision problem and the mechanization of theorem-proving in elementary geometry［J］. Science China: Mathematics, 1978, 21(2): 159-172.
［2］CHOU S C. Proving and discovering theorems in elementary geometries using Wu's method［D］. Austin: University of Texas, 1985.
［3］KAPUR D. Using Grbner bases to reason about geometry problems ［J］. Journal of Symbolic Computation, 1986, 2(4): 399-408.
［4］KAOUR D, SAXENA T, YANG L. Algebraic and geometric reasoning using dixon resultant［C］// Proceedings of the 1994 International Symposium on Symbolic and Algebraic Computation. New York: ACM, 1994: 99-107.
［5］HONG J. Can we prove geometry theorem by computing an example［J］. Science China: Series A, 1986, 16(3): 234-243.(洪加威.能用例证法来证明几何定理吗［J］.中国科学: A辑, 1986, 16(3): 234-243.)
［6］DENG M. The parallel numerical method of proving the constructive geometric theorem［J］. Chinese Science Bulletin, 1989, 34(31): 1066-1070.
［7］ZHANG J, YANG L, DENG M. The parallel numerival methods in mechanical theorem proving［J］. Theoretical Computer Science, 1990, 74(3): 253-271.
［8］YANG L, ZHANG J, LI C. A prover for parallel numerical verification to a class of constructive geometirc theorems［J］. Journal of Guangzhou University: Nature Science Edition, 2002, 1(3): 29-34.
［9］HOU X. Proving by examples[C]// Mathematics Mechanization and Application. London: Academic Press, 2000：231-251.
［10］ZHANG J. How does computer solve geometry problems: talking about automated reasoning ［M］. Guangzhou: Jinan University Press, 2000.(张景中.计算机怎样解几何题:谈谈自动推理［M］.广州: 暨南大学出版社, 2000.)
［11］CHOU S-C, GAO X-S, ZHANG J-Z. Machine proofs in geometry ［M］. Singapore: World Scientific,1994.
［12］YANG L, GAO X S, CHOU S-C, et al. Automated proving and discovering of theorems in non-Euclidean geometries［C］// Automated Deduction in Geometry. Berlin: Springer-Verlag, 1998: 171-188.
［13］LI C, RUAN W, ZHANG L, et al. Mathmatical theory of computer algebra system ［M］. Beijing: Tsinghua University Press, 2010. (李超,阮威,张龙,等. 计算机代数系统的数学原理［M］. 北京: 清华大学出版社, 2010.)
［14］CARR FERRO G, GALLO G, GENNARO R. Probabilistic verification of elementary geometry statements［C］// Workshop on Automated Deduction in Geometry. Berlin: Springer-Verlag, 1997, 1360: 87-101.
［15］SCHWARTZ J T. Fast probabilistic algorithms for verification of polynomical identities［J］. Journal of Association for Computing Machinery, 1980, 27(4): 701-717.
［16］BROWNAWELL W D. Bounds for the degrees in the Nullstellensatz［J］. Annals of Mathematics, 1987, 126:577-591.
［17］KOLLAR J. Sharp effective Nullstellensatz［J］. Journal of the American Mathematical Society, 1988, 1(4): 963-975.
［18］GALLO G, MISHRA B. Efficient algorithm and bounds for Wu-Ritt characteristic sets［J］. Progress in Mathematics, 1990, 94: 119-142.
［19］GALLO G, MISHRA B. Wu-Ritt characteristic sets and their complexity［J］. Mathematics and Theoretical Computer Science, 1991, 6: 111-136.
［20］TULONE D, YAP C, LI C. Randomized zero testing of radical expression and elementary geometry theorem proving ［C］// Proceedings of the 3rd International Workshop on Automated Deduction in Geometry. Berlin: Springer, 2001: 58-82.
［21］Index of /exact/core［EB/OL］.［2013-10-10］.http: //cs.nye.edu/exact/cpre/.
［22］YANG L, ZHANG J, HOU X. Nonlinear algebraic equations and theorem machine prove ［M］. Shanghai: Shanghai Scientific and Techincal Publishers, 1996. (杨路,张景中,侯晓荣.非线性代数方程组与定理机器证明［M］.上海:上海科技教育出版社,1996.)
［23］WANG D, YANG L, LI Z. Selected lectures in symbilc computation ［M］. Beijing: Tsinghua University Press, 2003.(王东明, 杨路, 李志斌.符号计算选讲［M］.北京:清华大学出版社, 2003.)
［24］CHOU S-C. An indroduction to Wu's method for mechanical theorem proving in geometry［J］. Journal of Automate Reasoning, 1988,4(3):237-267.
［25］CHOU S-C. Mechanical geometry theorem proving ［M］. Dordrecht: Reidel Publishing Company, 1988.
［26］WANG D. A new theorem discovered by computer prover ［J］. Journal of Geometry, 1989, 36(1/2): 173-182.

[1]	陈露张晓霞于洪. 基于先验知识的非负矩阵半可解释三因子分解算法[J]. 计算机应用, 0, (): 0-0.
[2]	李晓杰崔超然宋广乐苏雅茜吴天泽张春云. 基于时序超图卷积神经网络的股票趋势预测方法[J]. 计算机应用, 0, (): 0-0.
[3]	李宗正周恺卿丁雷欧云. 基于基因交换的自适应人工鱼群算法[J]. 计算机应用, 0, (): 0-0.
[4]	刘清华廖士中. 基于随机素描方法的在线核回归[J]. 计算机应用, 0, (): 0-0.
[5]	刘忠慧王梓宥闵帆. 近似概念的遗传生成算法及其推荐应用[J]. 计算机应用, 0, (): 0-0.
[6]	汪敏冯婷婷闵帆唐洪明闫建平廖纪佳. 页岩气储层预测的多标签主动学习算法[J]. 计算机应用, 0, (): 0-0.
[7]	王雅辉, 钱宇华, 刘郭庆. 基于模糊优势互补互信息的有序决策树算法[J]. 计算机应用, 2021, 41(10): 2785-2792.
[8]	任柯舟, 彭甫镕, 郭鑫, 王喆, 张晓静. 动态融合社交信息的社会化推荐[J]. 计算机应用, 2021, 41(10): 2806-2812.
[9]	张志浩, 林耀进, 卢舜, 郭晨, 王晨曦. 缺失标记下基于类属属性的多标记特征选择[J]. 计算机应用, 2021, 41(10): 2849-2857.
[10]	顾军华樊帅李宁宁张素琪. 基于知识图偏好注意力网络的长短期推荐模型及其更新方法[J]. 计算机应用, 0, (): 0-0.
[11]	王海起王志海李留珂孔浩然王琼徐建波. 基于网格划分的城市短时交通流量时空预测模型[J]. 计算机应用, 0, (): 0-0.
[12]	陈恒王思懿李正光李冠宇刘鑫. 基于关系记忆的胶囊网络知识图谱嵌入模型[J]. 计算机应用, 0, (): 0-0.
[13]	张成, 万源, 强浩鹏. 基于知识蒸馏的深度无监督离散跨模态哈希[J]. 计算机应用, 2021, 41(9): 2523-2531.
[14]	孙浩艺, 王传美, 丁义明. 基于隐藏层输出矩阵的极限学习机算法优化[J]. 计算机应用, 2021, 41(9): 2481-2488.
[15]	卞凌志, 王直杰. 基于增强多维多粒度级联森林的信用评分模型[J]. 计算机应用, 2021, 41(9): 2539-2544.

改进的几何定理机器证明的概率性算法

Improved probabilistic algorithm of mechanical geometry theorem proving

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics