点几何及其机器证明

There have been rich results about the theories and algorithms in the field of automated geometry theorem proving, but still cannot meet the needs of mathematics education. In recent years, with the development of information technology especially the network technology, people have more and higher expectations about artificial intelligence and pay considerable attention to human-like answering questions. Based on the mass point method which was established by the applicants, this project plans to further research on new algorithms which can automatically generate readable solutions for geometry problems. The new algorithms aim at producing the problem solving process which can comply with the mathematics curriculum test specification in basic education. The project includes the following contents: first, developing and improving the operation system of Mass Point Geometry to be a new operation system called Point Geometry; second, the mechanization algorithms on generating readable solutions for geometry problems under the operation system of Point Geometry; third, the mechanization method for transforming the solutions of form Point Geometry into human-like solutions. The results of this project will enrich or develop the theories and methods of automated reasoning in geometry and will have potential application prospect in education.

几何定理机器证明的理论和算法研究虽有了丰富的成果，但仍不能满足数学教育的需求。 近年来随着信息技术特别是网络技术的发展，人们对人工智能有了更多和更高的期望，其中对类人答题给予相当的关注。本课题拟在申请人所建立的质点法机器证明的基础上，进一步研究几何问题可读解答的自动生成算法；新算法旨在产生符合基础教育中数学课程测试规范的解题过程。课题的研究内容包括：（1）发展改进质点几何的运算系统为“点几何”系统；（2）“ 点几何”系统下几何问题可读解答自动生成的机械化算法；（3）“点几何”形式的解答转换为类人解答的机械化方法。本项目的成果将丰富与发展几何自动推理的理论和方法，并且有潜在的教育应用前景。

人们对几何学的代数形式已经进行了长期的深入的研究，并有了坐标系统、向量空间、质点几何以及其他几何代数体系等丰富成果。本项目提出，以质点几何学的原理和方法为基础，建立一个新的“点几何”运算系统，兼有向量方法、坐标方法和质点几何方法的长处而避免其缺点。. 本项目研究的主要内容包括：（1）发展改进质点几何的运算系统为点几何系统；（2）点几何系统下几何问题可读解答自动生成的机械化算法；（3）点几何恒等式方法；（4）点几何形式的解答转换为其他形式的类人解答的规律和方法。. 研究表明，点几何不仅符合数学直观，能方便地表达基本几何事实，而且有助于几何推理的简化。主要结果有：（1）基于点几何中定义的运算，可以分别建立处理仿射类几何问题以及度量几何问题的具有完全性的机械化算法；在Maple中实现的点几何证明器，能自动生成与手工媲美的证明过程；（2）基于点几何的各种运算，可以直接将命题的结论和条件分别用点几何表达式表示，然后找出结论和各条件间存在的一个在点几何的定义和运算下成立的恒等式，这种证明几何定理的方法叫点几何恒等式方法；（3）对吴方法的算法略加改进，就可以得到一种将结论表示为条件的线性组合的恒等式，这种恒等式本身就表明了命题成立，因此，吴方法本质上是一种恒等式方法；基于这个思想，可以发展不同形式的多种多样的恒等式证明方法，点几何恒等式方法只是其中的一种较优的表现形式；（4）点几何证明过程中的每一步，可以根据点几何与质点、向量、坐标及复数的关联，相应地转化为其他方法的证明步骤，且转化的过程可以程序化。. 本项目的成果丰富和发展了几何自动推理的理论和方法，同时在基础数学教育方面具有潜在的应用前景。