中文摘要：

向量法证明几何定理的机械化研究在二十多年前已经开始，但至今能生成可读向量法证明的完全性算法仅有基于面积消点法转化的一种方法，且所生成的证明的可读性通常不能令人满意。本课题拟在申请人所建立的质点法机器证明的基础上，发展一种适用于可构图几何定理的具有完全性的能自动生成可读向量证明的新算法并编程实现。新算法生成的解答将更接近人们常用的向量解题方法。课题的研究内容包括（1）向量处理两线相交的程序化方法；（2）向量法求解希尔伯特交点类命题的机械化方法；（3）向量法求解线性构造型几何命题的机械化方法。本项目的成果将丰富与发展几何自动推理的理论和方法，并且具有良好的教育应用前景。