摘要
为了实现几何自动推理的可读性证明,并提高推理效率,介绍了一个基于消点法的可构造性几何命题自动推理系统的设计与实现。该系统提供作图的方式接受用户的几何命题前提条件的输入,可以对初等几何中的大部分可构造性几何问题进行自动证明和求解,并生成可读的证明步骤,大大方便了初高等几何教育和相关研究者的需要。
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.
出处
《计算机应用》
CSCD
北大核心
2008年第11期2984-2986,共3页
journal of Computer Applications
关键词
几何定理自动证明
自动推理
消点法
可构造性几何命题
构图
automated geometry theorem proving
automated reasoning
point-eliminating method
structive geometry statements
graphic-drawing