Improved probabilistic algorithm of mechanical geometry theorem proving

doi:10.11772/j.issn.1001-9081.2014.07.2080

Journal of Computer Applications ›› 2014, Vol. 34 ›› Issue (7): 2080-2084.DOI: 10.11772/j.issn.1001-9081.2014.07.2080

• Artificial intelligence • Previous Articles Next Articles

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

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

陈明雁¹,曾振柄²

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

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

Abstract

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.

摘要：

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

CLC Number:

TP181

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

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

References

［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]	. Privacy preserving localization of surveillance images based on large vision models [J]. Journal of Computer Applications, 0, (): 0-0.
[2]	. Federated class-incremental learning method with multi-head self-attention for label semantic embedding [J]. Journal of Computer Applications, 0, (): 0-0.
[3]	Jingxin LIU, Wenjing HUANG, Liangsheng XU, Chong HUANG, Jiansheng WU. Unsupervised feature selection model with dictionary learning and sample correlation preservation [J]. Journal of Computer Applications, 2024, 44(12): 3766-3775.
[4]	Yifei SONG, Yi LIU. Fast adversarial training method based on data augmentation and label noise [J]. Journal of Computer Applications, 2024, 44(12): 3798-3807.
[5]	. Research review on explainable artificial intelligence in internet of things applications [J]. Journal of Computer Applications, 0, (): 0-0.
[6]	Jiachen YU, Ye YANG. Irregular object grasping by soft robotic arm based on clipped proximal policy optimization algorithm [J]. Journal of Computer Applications, 2024, 44(11): 3629-3638.
[7]	Zhijie LI, Xuhong LIAO, Yuanxiang LI, Qinglan LI. Disease sample classification algorithm by Bayesian network with gene association analysis [J]. Journal of Computer Applications, 2024, 44(11): 3449-3458.
[8]	Yuxin HUANG, Yiwang HUANG, Hui HUANG. Meta label correction method based on shallow network predictions [J]. Journal of Computer Applications, 2024, 44(11): 3364-3370.
[9]	HU Jie, ZHENG Qiyang, SUN Jun, ZHANG Yan. Multi-label classification model based on multi-relational label graph and local dynamic reconstruction learning [J]. Journal of Computer Applications, 0, (): 0-0.
[10]	Wenze CHAI, Jing FAN, Shukui SUN, Yiming LIANG, Jingfeng LIU. Overview of deep metric learning [J]. Journal of Computer Applications, 2024, 44(10): 2995-3010.
[11]	Chunyong YIN, Yongcheng ZHOU. Automatically adjusted clustered federated learning for double-ended clustering [J]. Journal of Computer Applications, 2024, 44(10): 3011-3020.
[12]	Feng CAO, Xiaoling YANG, Jianbing YI, Jun LI. Contradiction separation super-deduction method and application [J]. Journal of Computer Applications, 2024, 44(10): 3074-3080.
[13]	. Deep symbol regression method based on Transformer [J]. Journal of Computer Applications, 0, (): 0-0.
[14]	. RecipeFlavor: Recipe Recommendation Model Based on Flavor Embedding and Heterogeneous Graph Hierarchical Learning [J]. Journal of Computer Applications, 0, (): 0-0.
[15]	. Graph regularized Elastic Net Subspace Clustering [J]. Journal of Computer Applications, 0, (): 0-0.

Improved probabilistic algorithm of mechanical geometry theorem proving

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

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics