基于前推法的几何信息搜索系统

我们提出并实现了几何信息搜索系统（ＧＩＳＳ），它可用于找出所给几何图形的＂所有＂性质．记ＧＰ为一给定的几何谓词之集，ＬＭ为涉及ＧＰ中谓词的某些几何引理之集．若ＬＭ中的引理不引入新的几何元素，则用ＧＩＳＳ能找出所有能由ＬＭ中引理推出的几何性质．由于适当选择谓词和引理，合理组织数据和优化推理过程，对平面欧氏几何成功地实现了ＧＩＳＳ．它可以用于发现非平凡的几何性质，也可以作为其它几何定理机器证明系统的辅助工具使证明更为优美、简短和传统化．文末给出了几个例子和对１６１个几何问题运行的统计数据．

A REVIEW AND PROSPECT OF READABLE MACHINE PROOFS FOR GEOMETRY THEOREMS

在半世纪研究以后，在几何学证明的机械定理在自动化推理领域里成为了一个活跃研究话题。这评论在为包括搜索方法，没有坐标的方法，和正式逻辑方法的几何学定理产生可读的机器证明自动化上包含三条途径。关于这些途径的一些关键问题也被讨论。而且，作者为几何学定理为可读的机器证明建议三个进一步的研究方向，包括几何学不平等，聪明的几何学软件和机器学习。