质点几何定理机器证明的研究进展
Research Progress of Automated Particle Geometry Theorems Proving
摘要: 质点几何定理机器证明是当前几何定理机器证明领域内的一个研究热点。本文介绍了质点几何的基本理论。综述了质点几何定理机器证明近年来取得的一些比较显著的进展。比较了质点法和质点消去法这两种证明方法的优缺点。最后，展望了这个方向上需要进一步研究的问题。
Abstract: Nowadays, the automated particle geometry theorems proving is a new topic in automated rea-soning field. In this paper, we introduced firstly foundations of particle geometry theory, and then summarized the state of art of this topic in recent years. In addition, we compared two new auto-mated particle geometry theorems proving methods: the particle method and the particle elimi-nation method. Finally, we prospected some further research problems in this topic.
文章引用：胡晓璐, 江建国, 张媛. 质点几何定理机器证明的研究进展[J]. 应用数学进展, 2018, 7(12): 1490-1499. https://doi.org/10.12677/AAM.2018.712173

参考文献

[1] Tarski, A. (1948) A Decision Method for Elementary Algebra and Geometry. The RAND Corporation Press, Santa Monica.
[2] 吴文俊. 初等几何判定问题与机械化证明[J]. 中国科学, A辑, 1977(6): 507-516.
[3] Chou, S. (1984) Proving Elementary Geometry Theorems Using Wu’s Algorithm. In: Bledsoe, W. and Loveland, D., Eds., Au-tomated Theorem Proving: After 25 Years, AMS Contemporary Mathematics Series, 29, 243-286.
[4] Buchberger, B., Collins, G. and Kutzler, B. (1995) Algebraic Methods for Geometric Reasoning. Annual Review of Computer Sciences, 3, 85-119.
[5] Kutzler, B. and Stifter, S. (1986) On the Application of Buchberger’s Algorithm to Automated Geometry Theorem Proving. Journal of Symbolic Computation, 2, 389-397. [Google Scholar] [CrossRef] 
[6] Hong, J. (1986) Can Geometry be Proved by an Example? Scientia Sinica, 29, 824-834.
[7] Zhang, J. and Yang, L. (1989) Principles of Parallel Numerical Method and Sin-gle-Instance Method of Mechanical Theorem Proving. Mathematics in Practice and Theory, 1, 34-43.
[8] Zhang, J.Z., Chou, S.C. and Gao, X.S. (1995) Automated Production of Traditional Proofs for Theorems in Euclidean Geometry, I. The Hilbert Intersection Point Theorems. Annals of Mathematics and Artificial Intelligence, 13, 109-137. [Google Scholar] [CrossRef] 
[9] Chou, S.C., Gao, X.S. and Zhang, J.Z. (1996) Automated Generation of Readable Proofs with Geometric Invariants, II: Theorem Proving with Full-Angles. Journal of Automated Reasoning, 17, 349-370. [Google Scholar] [CrossRef] 
[10] Chou, S., Gao, X. and Zhang, J. (1993) Mechanical Geometry Theorem Proving by Vector Calculation. Proceedings of International Symposium on Symbolic and Algebraic Computation, ACM Press, New York, 284-291.
[11] Chou, S., Gao, X. and Zhang, J. (1994) Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems. World Scientific, Singapore. [Google Scholar] [CrossRef] 
[12] Yang, L., Gao, X. and Chou, S. (1997) Automated Production of Readable Proofs for Theorems in Non-Euclidean Geometries. Automated Deduction in Geometry, LNCS 1360, Springer-Verlag, 171-188. [Google Scholar] [CrossRef] 
[13] Chou, S.C., Gao, X.S. and Zhang, J.Z. (1996) Automated Generation of Readable Proofs with Geometric Invariants-I: Multiple and Shortest Proof Generation. Journal of Automated Reasoning, 17, 325-347. [Google Scholar] [CrossRef] 
[14] Zhang, J.Z. (2000) Points Elimination Methods for Geometric Problem Solving. Mathematics Mechanization and Applications, Academic Press, London, 175-202. [Google Scholar] [CrossRef] 
[15] 邹宇, 郑焕, 张景中. 仿射质点几何的可读机器证明[J]. 计算机应用, 2010, 30(7): 1989-1912.
[16] 邹宇. 几何代数基础与质点几何的可读机器明[D]: [博士学位论文]. 广州: 广州大学, 2010.
[17] Zou, Y. and Zhang, J. (2010) Automated Generation of Readable Proofs for Constructive Geometry Statements with the Mass Point Method. In: Schreck, P., Narboux, J. and Richter-Gebert, J., Eds., ADG 2010, LNAI 6877, 221-258.
[18] 吴文俊. 力学在几何中的一些应用[M]. 北京: 中国青年出版社, 1962.
[19] 张景中, 邹宇. 从“两点如何相加”谈起(上) [J]. 湖南教育, 2012, 6(2): 27-30.
[20] 张景中, 邹宇. 从“两点如何相加”谈起(下) [J]. 湖南教育, 2012, 6(2): 27-30.
[21] 莫绍揆. 质点几何学[M]. 重庆: 重庆出版社, 1992.
[22] 江建国, 苏贺靓, 高华. 质点几何定理证明的机器实现[J]. 科技视界, 2015(15): 96-97.
[23] 李辉. 质点几何定理的机器证明[D]: [硕士学位论文]. 大连: 辽宁师范大学, 2017.
[24] 张景中, 张传军, 郑焕, 等. SGARP中符号计算模块的实现及其应用[J]. 计算机研究与发展, 2014, 51(6): 1341-1351.
[25] 张传军, 邹宇, 郑焕, 等. 质点法在SGARP中的新发现[J]. 数学的实践与认识, 2014, 51(6): 302-311.

为你推荐