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

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