基于面向对象的几何定理自动证明系统设计与实现

针对几何定理自动证明的前推法实现方式,结合面向对象编程工具的特点,实现了一个原型系统。该系统结构简单、清晰,可扩展性强,并能产生可读证明过程。实例分析说明了该原型的有效性。

基于消点法的几何自动推理系统实现

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