马库恩 用机器证明数学猜想  

作　　者：尼克 

机构地区：[1]乌镇智库

出　　处：《环球人物》2024年第24期96-97,共2页Global People

摘　　要：机器定理证明是人工智能中最古老也最困难的研究领域。在这一领域,威廉·马库恩(1953-2011)可以称得上是最杰出的实干家,他创立的一阶定理证明器Otter是上世纪90年代基于逻辑的定理证明器的集大成者,影响了当时整个定理证明领域的理论和实践。说起机器定理证明,需要溯源到著名的阿贡实验室。

关 键 词：定理证明器 数学猜想 人工智能 机器证明 实验室 库恩 实干家 

分 类 号：G63[文化科学—教育学]