[敬请读者注意] 本人保留本文的全部著作权利。如果哪位读者使用本文所描述内容，请务必如实引用并明白注明本文出处。如果本人发现任何人擅自使用本文任何部分内容而不明白注明出处，恕本人在网上广泛公布侵权者姓名。敬请各位读者注意，谢谢！

自动定理发现领域的创始者 - 沃斯

程京德 

    伟大的盲人学者拉里·沃斯(Larry T. Wos, 1930-2020)是美国数学家、数理逻辑学家、计算机科学家，是自动推理领域的先驱者之一，自动定理发现领域的创始者。

    沃斯于1988年出版了“Automated Reasoning: 33 Basic Research Problem”一书 [1]，提出了在自动推理领域中的33个未解问题，其中第31个问题就是“自动定理发现问题(the problem of Automated Theorem Finding, ATF)”[1,2]，从而开创了“自动定理发现”这一极具挑战性和应用性的领域。

    沃斯定义“自动定理发现问题”为：“相对于证明猜测的定理，什么性质可以被识别出来以期允许一个自动推理程序发现新的并且有趣的定理？(What properties can be identified to permit an automated reasoning program to find new and interesting theorems, as opposed to proving conjectured theorems?)”[1,2]

    “自动定理发现问题”最重要也是最困难的要求是，与自动地证明由用户预先提供的推测定理相反，它要求识别和建立自动推理程序可用的一般性判别标准，用以自动地发现某个领域（注意，并非一定是数学领域）中的一些定理（亦即，并非单个特殊定理），这些定理必须被该领域的理论家评价为新的并且有趣的定理。解决这个问题的重要意义是显而易见的，因为满足要求的自动推理程序可以为各个领域的科学家提供极大的帮助。

    “研究问题31寻求自动推理程序可以用来发现有趣定理的标准，而不是证明用户提供的推测定理。特别地，由于推理程序可以被指令得出一些(可能很大的)结论集合，研究问题31要求允许程序从那些结论中选择对应于感兴趣的结果的结论(如果有的话)的标准。(Research Problem 31 asks for criteria that an automated reasoning program can employ to find interesting theorems, in contrast to proving conjectured theorems supplied by the user. In particular, since a reasoning program can be instructed to draw some (possibly large) set of conclusions, Research Problem 31 asks for criteria that permit the program to select from those conclusions the ones (if any) that correspond to interesting results.)”[1,2]

    “对研究问题31的解决方案的测试取决于应用推理程序所做研究之领域的专家。提出的解决方案必须使一个推理程序能够选择结果，例如，群论理论家评价为有趣的定理。显然，解决这个问题将是有意义的，因为相应的推理程序可以为各个领域的研究者提供帮助。(The test for a solution to Research Problem 31 rests with the expert in the field under investigation by the reasoning program. The proposed solution must enable a reasoning program to select result that, for example, the group theorist evaluates as interesting theorems. Obviously, solving this problem would be significant because of the assistance that the corresponding reasoning program could provide for researchers in various fields. )”[1,2]

    沃斯提出“自动定理发现问题”已经三十几年，但是该问题至今仍未被完全解决。

    沃斯1930年出生于美国芝加哥市，先天失明，2020年以90岁高龄逝世。沃斯1950年毕业于芝加哥大学，1954年在芝加哥大学获得数学硕士学位，1957年在伊利诺伊大学厄巴纳-香槟分校获得博士学位。沃斯自1957 年起的整个职业生涯都在芝加哥附近阿贡市的阿贡国家实验室数学与计算机科学部门(the Mathematics and Computer Science (MCS) Division of the Argonne National Laboratory)度过 [3,4]。

    沃斯从1963年起就开始从事自动定理证明方面的工作，是自动定理证明领域的先驱者之一。沃斯是自动推理协会(the Association for Automated Reasoning, AAR)的创始人(1983年)，并于 1983 年至 2020 年一直担任 AAR 的主席/会长。沃斯还是自动推理杂志(the Journal of Automated Reasoning, JAR)的创始人及主编(1985年)，以及自动演绎国际会议(the international Conference on Automated Deduction, CADE)的创始人(1975年) [3,4]。

    1982年，沃斯与史蒂夫·温克 (Steve Winker) 共同荣获美国数学学会颁发的首届自动定理证明奖(the Automated Theorem Proving Prize)；1992年，沃斯荣获自动演绎国际会议颁发的首届赫尔布兰德奖 (The Herbrand Award for Distinguished Contributions to Automated Reasoning) [3,4]。

    Tim Andrew Obermiller 在1997年介绍沃斯的一篇文章“他攀上顶峰(Top of his game)”的首句写道：“数学先驱拉里·沃斯曾被告知一个盲人将无法实现他所设定的目标，但他通过学习如何克服困难赢得了成功。(Told that a blind person would fail at what he set out to achieve, math pioneer Larry Wos won by learning how to beat the odds.)”[3]

    笔者本人从1993年开始在自动定理发现领域进行研究工作，提出以相关逻辑作为自动定理发现的逻辑基础，开发了 EnCal 和 FreeEnCal 自动前推机用于基于强相关逻辑的自动推理，提出给科学家们提供认识程序设计方法论及工具来“设计”并“自动化”其科学发现过程；笔者主张，实现人工通用智能的关键必由之路是基于强相关逻辑的形式理论自动定理发现 [5-15]。

    图灵奖(1975年)及诺贝尔经济学奖(1978年)获奖者，美国卡内基梅隆大学教授赫伯特·亚历山大·西蒙(司马贺，Herbert Alexander Simon，1916-2001)及其学生们多年来一直在科学发现自动化这个方向上工作。下图为西蒙教授在1995年AAAI暑期“Systematic Methods of Scientific Discovery”研讨会上与笔者讨论自动定理发现问题时留给笔者的签名。

参考文献

[1] L. Wos, “Automated Reasoning: 33 Basic Research Problem,” Prentic-Hall, 1988.

[2] L. Wos, “The Problem of Automated Theorem Finding,” Journal of Automated Reasoning, Vol. 10, No. 1, pp. 137-138, 1993.

[3] T. A. Obermiller, “Top of his game,” The University of Chicago Magazine, April 1997. 

[4] M. P. Bonacina, “In Memoriam: Larry Wos,” AAR Newsletter No. 132, Association for Automated Reasoning, September 2020. 

[5] J. Cheng, “A Relevant Logic Approach to Automated Theorem Finding,” Proceedings of the Workshop on Automated Theorem Proving attached to International Symposium on Fifth Generation Computer Systems 1994, pp. 8-15, Tokyo, Japan, December 1994. 

[6] J. Cheng, “Entailment Calculus as the Logical Basis of Automated Theorem Finding in Scientific Discovery,” in R. Valdes-Perez (Ed.), “Systematic Methods of Scientific Discovery: Papers from the 1995 Spring Symposium,” AAAI Technical Report SS-95-03, pp. 105-110, AAAI Press, March 1995.

[7] J. Cheng, “EnCal: An Automated Forward Deduction System for General-Purpose Entailment Calculus”, in: N. Terashima, and E. Altman (eds.), Advanced IT Tools, Proceedings of the IFIP World Conference on IT Tools, IFIP 96 - 14th World Computer Congress, pp. 507-514, Chapman & Hall, London, September 1996.

[8] J. Cheng, S. Nara, and Y. Goto, “FreeEnCal: A Forward Reasoning Engine with General-Purpose”, in: B. Apolloni, R. J. Howlett, and L. C. Jain (eds.), Knowledge-Based Intelligent Information and Engineering Systems, 11th International Conference, KES 2007, Lecture Notes in Artificial Intelligence, Vol. 4693, pp. 444-452, Springer-Verlag, September 2007.

[9] J. Cheng, “A Strong Relevant Logic Model of Epistemic Processes in Scientific Discovery,” in E. Kawaguchi, H. Kangassalo, H. Jaakkola, and I. A. Hamid (eds.), Information Modeling and Knowledge Bases XI, Frontiers in Artificial Intelligence and Applications, Vol. 61, pp. 136-159, IOS Press, February 2000.

[10] J. Cheng, “Automated Knowledge Appreciation: A Relevant Reasoning Approach to Expand Our Knowledge and Increase Its Value Automatically,” Proceedings of the 14th IEEE International Conference on Cognitive Informatics & Cognitive Computing, pp. 175-183, Beijing, China, IEEE Computer Society Press, July 2015.

[11] H. Gao, Y. Goto, and J. Cheng, “A Systematic Methodology for Automated Theorem Finding,” Theoretical Computer Science, Vol. 554, pp 2-21, Elsevier B.V., October 2014.

[12] H. Gao and J. Cheng, “An Epistemic Programming Approach for Automated Theorem Finding,” Proc. 14th IEEE International Conference on Cognitive Informatics & Cognitive Computing, Beijing, China, IEEE Computer Society Press, July 2015.

[13] 程京德，“相关推论与强相关逻辑”，科技导报，Vol. 34, No. 7, pp. 39-47, 2016.

[14] 程京德，“强相关逻辑及其应用（上）、（中）、（下）”，微信公众号“数理逻辑与哲学逻辑”，科学网博客，2023年6月18日、2023年8月8日、2023年8月12日。

[15] 程京德，“实现人工通用智能的关键必由之路 - 基于强相关逻辑的形式理论自动定理发现”，微信公众号“数理逻辑与哲学逻辑”，科学网博客，2023年10月19日。

微信公众号“数理逻辑与哲学逻辑”