赫尔布朗特定理开启自动定理证明的大门

1930年，年仅22岁的法国“小毛头”赫尔布朗特（Jacques
Herbrand，1908-1931）在登山时遇难的前一年给我们留下了一条数理逻辑的基本定理：赫尔布朗特定理。这条定理有什么意义呢？

大家知道，在数理逻辑里面，引入量词符号“∃”与“∀”，是很重要的，但是，对于数学自动鼎定理证明而言，量词符号“∃”与“∀”就是累赘。怎么办呢？

在所谓“一阶逻辑”里面，符号“∃”与“∀”允许出现在逻辑公式里面，如果设法将其消除，那么“一阶逻辑“就变成传统的命题逻辑公式（类似布尔逻辑公式）了。赫尔布朗特定理证明了这一结论，并且给出了消除量子符号的步骤，开启了现代自动定理证明的大门。

后人为了纪念赫尔布朗特的重要贡献，从1992年开始，在机器自动定理证明研究邻域设立了”赫尔布朗特奖“，奖金额度虽然不高（1000美元），但是学术荣誉（含金量）极高。1997年，我国著名数学家吴文俊（Wu
wenjun）教授荣获该奖，以表彰他对初等几何定理机械化自动证明的成果。

近日，北大、清华为争夺今年高考“状元”打得不可开交，也不怕丢人。我国高考状元有几个人能够取得类似赫尔布朗特的学术成就？原因是什么？我们要知道一个事实：数学大师冯.纽曼是赫尔布朗特的指导老师！所谓”名师出高徒“。我国的数学名师在何方？

袁萌
7月4日