如何在解题过程中积累例子

数学大师陈省身教授曾经说过:"一个好的数学家与一个蹩脚的数学家,差别在于前者有很多具体的例子,后者则只有抽象的理论".这句话对一般的解题者来说也是正确的,可以这么说:一个好的解题者与一个蹩脚的解题者,差别在于前者有很多具体的例子,后者则只有抽象的公式和定理.……     

可由用户持续发展的几何自动推理平台

提出并实现了可由用户持续发展的几何自动推理平台(SGARP).它由知识库、知识编辑器、信息库、推理引擎、信息查询窗口和动态几何作图系统等六部分组成.在这个平台上,用户可以添加几何对象、谓词和规则,也可以综合使用多种推理方法进行推理.     

质点法在SGARP中的新实现

可持续发展的几何自动推理平台(SGARP)支持用户发展多种多样基于规则的机器自动推理或人机交互推理方法,但缺乏处理符号计算的模块,其解题能力仍有待加强.质点法是最近发展的继面积法之后又一个能对可构造型几何命题生成可读机器证明的具有完全性的算法.基于一种在SGARP中快捷实现符号计算功能的方法,对质点法机器证明算法进行了新的实现.新添加的质点法模块使得用户能更便捷地验证更多的几何定理,从而使SGARP能更好地满足用户学习与发展几何机器推理的需求.