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

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