可构图几何定理向量法可读机器证明的完全性新算法

Researchers began to develop the vector method for automated geometry theorem proving 20 years ago, but there are still no other complete algorithms for generating readable vector proofs except the vector method which was developed according to the area method, and moreover, the readability of the machine vector proofs is unsatisfactory. This project plans to develop a new complete algorithm for generating readable vector proofs for constructive geometry theorems automatically based on the new machine proving method, the mass point method which was established recently by the applicants. The machine proofs generated by the new algorithm will be closer to human’s usual vector approach to geometry problems. The project includes the following contents: first, the mechanical steps for dealing with the intersections of two lines by way of normal vector calculation; second, the mechanical method for solving the Hilbert intersection point statements by our new vector method; third, the mechanical method for solving the linear constructive geometry statements. 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）向量法求解线性构造型几何命题的机械化方法。本项目的成果将丰富与发展几何自动推理的理论和方法，并且具有良好的教育应用前景。

几何定理向量法可读机器证明的完全性算法，以前仅有基于面积消点法转化的一种方法，且所生成的证明的可读性通常不令人满意．基于课题负责人前期建立的质点法机器证明的机械化模式，本项目从向量的基本性质出发，引进了支持程序化地处理两线交点的向量公式，采用了欧氏平面上向量的基本性质以描述各种度量关系，发展了一种能适用于构造型几何命题的具有完备性的向量法机器证明新算法，并在Maple中实现．对350个几何命题的运行结果显示，基于本算法实现的证明器不仅高效，而且所生成的解答过程更接近人们常用的向量解题方法．