Gordon M J C
University of Cambridge Computer Laboratory, William Gates Building, 15 JJ Thomson Avenue, Cambridge CB3 0FD, UK
Philos Trans A Math Phys Eng Sci. 2015 Apr 13;373(2039). doi: 10.1098/rsta.2014.0234.
Robin Milner's paper, 'The use of machines to assist in rigorous proof', introduces methods for automating mathematical reasoning that are a milestone in the development of computer-assisted theorem proving. His ideas, particularly his theory of tactics, revolutionized the architecture of proof assistants. His methodology for automating rigorous proof soundly, particularly his theory of type polymorphism in programing, led to major contributions to the theory and design of programing languages. His citation for the 1991 ACM A.M. Turing award, the most prestigious award in computer science, credits him with, among other achievements, 'probably the first theoretically based yet practical tool for machine assisted proof construction'. This commentary was written to celebrate the 350th anniversary of the journal Philosophical Transactions of the Royal Society.
罗宾·米尔纳的论文《使用机器辅助严格证明》介绍了自动化数学推理的方法，这些方法是计算机辅助定理证明发展历程中的一个里程碑。他的思想，尤其是他的策略理论，彻底改变了证明助手的架构。他使严格证明自动化的方法，特别是他在编程中的类型多态性理论，为编程语言的理论和设计做出了重大贡献。他因“可能是第一个基于理论且实用的机器辅助证明构建工具”等成就，被授予1991年美国计算机协会（ACM）的图灵奖，这是计算机科学领域最负盛名的奖项。这篇评论文章是为庆祝《皇家学会哲学学报》创刊350周年而撰写的。
