人工智能名人堂第19期 | 早逝的天才-埃尔布朗
丘吉尔曾说过，“The longer you can look back, the farther you can look forward. (回顾历史越久远，展望未来就越深远)”，为纪念人工智能领域做出杰出贡献的先辈与开拓者们，鼓励更多后起之秀投身该领域，人工智能国际杂志《IEEE Intelligent Systems》自2006年始至今陆续推选出了60位人工智能专家(参看《诺伯特·维纳奖得主王飞跃 | AI 名人堂，世界人工智能60年60位名人榜》)。德先生自10月31日起，已定期于每周一在微信公众号（D-Technologies）上发布人工智能名人堂60位成员的相关介绍。往期内容可查看延伸阅读。
1931年夏在阿尔卑斯山度假时，不幸遇险身亡，年仅23岁。埃尔布朗的主要贡献在数理逻辑和近世代数方面。他建立的埃尔布朗定理是量化理论的一个基本命题，已成为机器证明的基础。在近世代数方面，他发表了十几篇有关类域论的论文，丰富了代数数域的阿贝尔扩张理论。
埃尔布朗登山前拍的最后一张照片
埃尔布朗定理
在逻辑学中，埃尔布朗定理(Herbrand's theorem)建立了命题逻辑计算和谓词逻辑计算之间的关系，因此埃尔布朗定理可能是一种已知的确定手段来判断一个命题的命题逻辑计算是否是有限的，对于一个含有复杂谓词的公式，它的谓词逻辑计算也起到同样的判断。通过对埃尔布朗定理的应用，部分解决回答了上述问题。但是虽然有Gödel(哥德尔)，Tarski(塔尔斯基)，Church(邱奇)，Turing(图灵)和其他科学家在逻辑学领域中卓越的研究成果，但是至今不存在一个算法，能够决定一个普遍公式的谓词逻辑计算是否是可计算的这样一个问题，我们不知道这个算法是否是可以被证明的。
前束范式
在谓词演算中，一个公式是前束范式的，如果它可以被写为量词在前，随后是被称为矩阵的非量化部分的字符串。所有一阶公式都逻辑等价于某个前束范式公式。
可以用公式在如下重写规则下的逻辑等价来证实：
它们的存在对偶：
这里的x在Q中是自由的，并注意通过这些规则的持续应用所有量词都可以移动到公式的前面。
备注：小编目前搜集整理的雅克·埃尔布朗的资料有限，欢迎有相关文章或者信息的读者在下方留言，或者联系小编整理发布这位年少成名却不幸早逝的天才的故事。
延伸阅读
德先生精彩文章回顾
在公众号会话位置回复以下关键词，查看德先生往期文章！
人工智能｜类脑研究｜人机大战｜机器人
虚拟现实｜无人驾驶｜智能制造｜无人机
科研创新｜网络安全｜数据时代｜区块链
……
更多精彩文章正在赶来，敬请期待！
点击“阅读原文”，移步求知书店，可查阅选购德先生推荐书籍。