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

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-08-01 出版日期:2014-07-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-08-01 Published:2014-07-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]. 《计算机应用》唯一官方网站, 2024, 44(12): 3766-3775.
[4]	宋逸飞, 柳毅. 基于数据增强和标签噪声的快速对抗训练方法[J]. 《计算机应用》唯一官方网站, 2024, 44(12): 3798-3807.
[5]	赵小阳许新征李仲年. 物联网应用中的可解释人工智能研究综述[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[6]	余家宸, 杨晔. 基于裁剪近端策略优化算法的软机械臂不规则物体抓取[J]. 《计算机应用》唯一官方网站, 2024, 44(11): 3629-3638.
[7]	李志杰, 廖旭红, 李元香, 李青蓝. 基于基因关联分析的贝叶斯网络疾病样本分类算法[J]. 《计算机应用》唯一官方网站, 2024, 44(11): 3449-3458.
[8]	黄雨鑫, 黄贻望, 黄辉. 基于浅层网络预测的元标签校正方法[J]. 《计算机应用》唯一官方网站, 2024, 44(11): 3364-3370.
[9]	胡婕郑启扬孙军张龑. 基于多关系标签图和局部动态重构学习的多标签分类模型[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[10]	柴汶泽, 范菁, 孙书魁, 梁一鸣, 刘竟锋. 深度度量学习综述[J]. 《计算机应用》唯一官方网站, 2024, 44(10): 2995-3010.
[11]	尹春勇, 周永成. 双端聚类的自动调整聚类联邦学习[J]. 《计算机应用》唯一官方网站, 2024, 44(10): 3011-3020.
[12]	曹锋, 杨小玲, 易见兵, 李俊. 矛盾体分离超演绎方法及应用[J]. 《计算机应用》唯一官方网站, 2024, 44(10): 3074-3080.
[13]	许鹏程何磊李川钱炜祺赵暾. 基于Transformer的深度符号回归方法[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[14]	颜文婧王瑞东左敏张青川. 基于风味嵌入异构图层次学习的食谱推荐模型[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[15]	郭书剑余节约尹学松. 图正则化弹性网子空间聚类[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.

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

Improved probabilistic algorithm of mechanical geometry theorem proving

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics