Abstract: In order to realize the readable proofs in geometry and improve the efficiency of reason, the design and implementation of an automatic reasoning system for structive geometry statements was introduced in the paper. Users can input the prerequisites of geometry statements by graphic-drawing method that the system provided. Most structive geometry statements in elementary geometry can be proved and resolved automatically with readable proofs, which can meet the needs of education and research on elementary or high geometry.

Key words: automated geometry theorem proving, automated reasoning, point-eliminating method, structive geometry statements, graphic-drawing

摘要： 为了实现几何自动推理的可读性证明，并提高推理效率，介绍了一个基于消点法的可构造性几何命题自动推理系统的设计与实现。该系统提供作图的方式接受用户的几何命题前提条件的输入，可以对初等几何中的大部分可构造性几何问题进行自动证明和求解，并生成可读的证明步骤，大大方便了初高等几何教育和相关研究者的需要。

关键词: 几何定理自动证明, 自动推理, 消点法, 可构造性几何命题, 构图