[00116288]几何自动作图方法、软件与应用

几何自动推理较多关注机器证明，但是工程应用领域经常遇到的问题可以归结为几何自动作图，即实现复杂、大规模几何图形作图的机械化。该项目提出几何自动作图的全局延拓法、C-树分解方法与LIMd方法，可以将大型问题分解为某种极小的“模式”，完整解决了几何图形的自动生成问题，使得用传统方法所不能解决的大型问题得以快速求解，以此为基础实现了自动推理平台的应用模块MMP/Geometer；以几何自动作图方法为基础解决了长期公开得P3P空间定位问题，给出了其解的个数的完全分类与完整解析解，并以此为基础发展了求解P3P问题的高效完整算法。　　全局延拓法的审稿意见认为是“几何自动推理又一重要突破(significant breakthrough)”。P3P问题的论文在机器智能与视觉方面权威杂志IEEE T. PAMI 发表为regular paper。 MMP/Geometer 被国外专家称为”两个重要与具有代表性的几何推理系统之一(Caffera, ADG, 2000)”, “最精良(most sophisticated)的证明系统”(Loveland, AI Mag，99)，“一个杰作(masterpiece)，代表了几何定理证明器的当前水平.”（Bortolossi，2002），99年获第四届亚洲数学技术大会“最佳论文”奖。