短 课 程

内容提要：几何定理的机器证明是自动推理和符号计算领域最活跃的分支之一。以吴方法为代表的代数方法是在计算机上证明和发现几何定理，解决各种几何问题的有效工具。本课程回顾几何定理机器证明的历史和发展，概述吴方法的基本思想和原理，介绍几何代数方法、演绎数据库方法和例证法，并报告有关结果和该学科的现状。