吴方法

70年代后期，在计算机技术大发展的背景下，吴文俊继承和发展了中国古代数学的传统（即算法化思想），转而研究几何定理的机器证明，彻底改变了这个领域的面貌，是国际自动推理界先驱性的工作，被称为“吴方法”，产生了巨大影响。吴的研究取得了一系列国际领先成果并已应用于国际上当前流行的符号计算软件方面。

定义70年代后期，在计算机技术大发展的背景下，吴文俊继承和发展了中国古代数学的传统（即算法化思想），转而研究几何定理的机器证明，彻底改变了这个领域的面貌，是国际自动推理界先驱性的工作，被称为“吴方法”，产生了巨大影响。

机器证明机器证明是使用计算机证明定理，也称为定理的机械证明或自动证明。作为计算机科学的一个重要课题，它的研究与发展至今约有50年的历史。

机器证明研究领域的范围要广泛得多。在国外则更一般地叫做自动推理。我们把几何定理机器证明和非线性代数方程组作为主攻方向，一方面是因为吴文俊先生在70年代的突出工作，使中国在此方向上具有了领先的优势；另一方面，这两个方向有鲜明的应用背景，近年来在机器证明领域也确是十分活跃的，值得重视。由于传统的兴趣和多种原因，几何定理的机器证明在自动推理的研究中占有重要的地位。

人物简介1940年毕业于上海交通大学数学系。1979年至现在任中国科学院系统科学研究所副所长、名誉所长、研究员。

吴文俊院士是著名的数学家，他的研究工作涉及到数学的诸多领域。在多年的研究中取得了丰硕成果。其主要成就表现在拓扑学和数学机械化两个领域。他为拓扑学做了奠基性的工作。他的示性类和示嵌类研究被国际数学界称为“吴公式”，“吴示性类”，“吴示嵌类”，至今仍被国际同行广泛引用，影响深远，享誉世界。

用计算机自动证明某一类型几何定理，甚至某一种几何全部定理的原理和方法。从理论角度看，几何定理的机器证明要经历公理化、代数化与坐标化、机械化等步骤，才能编制程序并在计算机上实现。可用机器证明的几何定理（主要是初等几何的定理）有三种不同类型，与之对应则有三种不同的机器证明方法。每一类型定理的机器证明都必须假设代数化与坐标化已经完成，而且可把几何定理的证明问题化为一些代数关系式的处理问题。①第一类型定理的特征是假设部分的所有代数关系式对于某些特定变量都必须是线性的，包括一类构造型的纯交点定理，其对应的机器证明方法称为希尔伯特方法；②第二类型定理的特征是假设和终结部分的代数关系式都可用多项式的方程来表示，其对应的机器证明方法是中国数学家吴文俊首先提出的，称为吴文俊方法；③第三类型定理的特征是假设和终结部分可以是任意的多项式等式或不等式，但其系数必须在一实闭域中，因而原来的几何必须有次序关系，其对应的机器证明方法称为塔斯基方法。这三种方法各有其适用范围，但就可以通用的那些定理证明问题来说，希尔伯特法效率最高而塔斯基法效率最低，但是前者的适用范围很窄。1980年在 HP9835A机上，用吴文俊方法成功地证明了勾股定理、西姆逊线定理、帕普斯定理、帕斯卡定理、费尔巴哈定理，并在45个帕斯卡点中发现了20条帕斯卡圆锥曲线，这种方法还推广到微分几何，将微分几何曲线论中的贝屈朗定理推广到仿射微分几何。吴文俊的研究成果引起了国际学术界的重视。1

本词条内容贡献者为:

胡建平 - 副教授 - 西北工业大学