质点法在SGARP中的新实现

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

New Implementations of the Mass Point Method in SGARP

The SGARP(sustainable geometry automated reasoning platform) supports users to develop varieties of rule-based machine proving methods or human-machine interactive reasoning methods,but it is short of the modules of symbolic computation and its ability of solving problems needs to be strengthened.The mass point method,which is effective against constructive statements in unordered geometry,is another complete algorithm for automated geometry theorem proving after the area method.Based on a convenient way of implementing the symbolic computation modules in SGARP,this paper implements the mass point method again in a new way.Newly added mass-point-method modules enable users to test more geometry theorems more easily,thus the SGARP can satisfy better the need of users' learning and developing geometry theorem reasoning.