数学定理证明机械化的中国学派（I）

1997年，吴文俊院士获得赫尔布朗特奖，说明了什么呢？首先，我们必须明确的是：赫尔布朗特奖是当今国际数学界自动定理证明研究领域的最高学术奖项。该奖项的授予标志着国际学术界（同仁）对获奖项目的一致认可。

回顾历年来，赫尔布朗特获奖者的名单如下：

Larry
Wos (1992)

Woody
Bledsoe (1994)

John
Alan Robinson (1996)

Wu
Wenjun (1997，吴文俊）

Gérard
Huet (1998)

Robert
S. Boyer and
JStrother Moore (1999)

William
W. McCune (2000)

Donald
W. Loveland (2001)

等等（省略）

Melvin
Fitting (2012)

CGreg
Nelson (2013)

Robert
L. Constable (2014)

我们要注意到，位于吴文俊之前的赫尔布朗特获奖者是John
Alan Robinson，此人是数理逻辑“消解原理”（Resolutionprinciple）的创始人，该”消解原理“是其他大多数数学自动定理证明的基本依据。可以说，吴文俊方法是“另类”（纯粹代数方法，不是主流），在过去数十年里面，一般而言，“吴方法”是不被国际学界所认可的。但是，后来学界对“吴方法”的态度为什么发生了转变？请看下文：数学定理证明机械化的中国学派（II）。

袁萌
7月4日