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

自动定理发现

程京德

“自动定理发现(Automated Theorem Finding, ATF)”，是美国数学家 Larry Wos 于 1988 年提出的自动推论(automated reasoning)领域中的 33 个未解决基本研究问题之一:  “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]  ATF 问题被提出 20 多年来，至今仍未完全解决。ATF 问题有几个基本要求：（1）要求“发现”而不是“证明”，（2）要求发现“新”的并且“有趣”的定理（因此，形式地定义清楚“新”和“有趣”就是必要的），（3）要求识别出那些“特性”使得能够让自动推论程序发现定理。正是这几个要求中包含的一般性，使得该问题成为一个难题；然而也正是因为这些一般性，使得该问题之解决意义重大，应用广泛。

笔者在 1994-1995 年提出了基于强相关逻辑的推论来一般地解决 ATF 问题的研究方向并且一直在此方向上工作 [3-8]。本文试图尽可能通俗地简单介绍 ATF 问题的背景、笔者的基本想法和工作进展、并且给出一些展望。

首先，自动推论或者自动演绎(automated deduction)的历史源头可以追溯到 20 世纪 50 年代 [9]。美国数学家 Martin Davis 在 1954 年编写了一个自动演绎证明程序来实现波兰逻辑学家 Presburger(Mojzesz Presburger, 1904-1943?) 在 1929 年提出的一个关于 Presburger 算术(Presburger arithmetic) 的判定问题算法，试图自动地判定一个给定 Presburger 算术命题的真伪。由于 Presburger 的判定算法具有指数复杂性，Davis 的程序当然没有得到什么满意的结果 [9,10]。

美国计算机科学家 Newell(A. Newell, 1927-1992, 1975 年图灵奖获得者),  Shaw(J.C. Shaw, 1922-1991) 和 Simon(H.A. Simon, 1916-2001, 1975 年图灵奖获得者, 1978 年诺贝尔经济学奖获得者)在 1955-1956 年开发了一个称为“逻辑理论家(Logic Theorist)”的自动演绎证明程序（被称为第一个真正的人工智能程序），试图自动地判定一个给定经典命题逻辑(演算)命题的真伪 [11]。逻辑理论家成功地自动证明了怀德海和罗素的名著“数学原理(Principia Mathematica)”中命题逻辑(演算)部分的 38 个定理 [9,11]。

华裔美国逻辑学家王浩(H. Wang, 1921-1995)在 1958 年用汇编语言开发了三个针对经典一阶谓词逻辑(演算)的自动演绎证明程序，在 IBM704 计算机上用不到 9 分钟的计算时间自动证明了怀德海和罗素的名著“数学原理(Principia Mathematica)”中一阶谓词逻辑(演算)部分的全部定理（350条以上）[12,13,14]。

美国逻辑学家、计算机科学家 John Alan Robinson 在 1965 年发表了被称为“归结原理(resolution principle)”的反证方法 [15]，从而导致此后相当长时间内对归结原理进行改进和应用的大量工作，并且成为支持现今许多自动定理证明器的基本工作原理。

我国数学家吴文俊在 1977 年发表了被称为“吴方法”的关于初等几何的快速判定算法，能够被用来证明不包括相对位置关系（“在……之间”）的初等几何定理 [16]；该算法是基于代数几何理论而不是明显地基于逻辑的。

美国数学家 Art Quaife 在 1990 年前后用自动定理证明器 OTTER 证明了公理集合论的大约 400条定理，初等数论的大约 1200 条定理和定义，欧氏几何的几十条定理，以及哥德尔的不完全性定理 [17]。

根据对上述背景研究工作的考察，笔者曾经归纳了下列事实 [3-8]：

（1） 直到1988年Wos提出ATF问题之前（甚至现在），自动推论/演绎研究领域几乎所有的工作都是关于自动定理证明的。

（2） 几乎所有关于自动定理证明的工作，都是以证明数学定理为目标的。

（3） 所有基于逻辑的自动定理证明的工作，都是基于经典数理逻辑或者其经典保存扩张(classical conservative extension)的，无一例外。

（4） 所有基于逻辑的自动定理证明器，其基础逻辑系统都是内含的，也就是说，是编制在自动定理证明器程序当中，而不是在执行时作为输入数据给予自动定理证明器程序的。

（5） 因为证明仅仅是确证已知或者假设的结论而不是发现以往未知的新结论，所以自动推论/演绎以往工作的实际应用范围一直很有限。

“推论(reasoning)”是从给定的前提（试图为新结论提供证据的已知事实或预设假说）推导出新结论的过程，是从我们的已知或预设（亦即，前提）到达预先未知（亦即，新结论）从而获取新知识、扩展已有知识的过程。一个推论过程一般是由一系列被称为推断(argument)或者推理(inference)的步骤有序地构成的。

“发现(discovery, finding)”是寻找出或者揭示出某个前所未知事物的过程。对于任何发现，其被发现的事物及其真伪应该是在发现过程完成之前预先未知的，否则，就完全没有必要去发现已知的事物了。由于推论是从给定前提获得预先未知的新结论之唯一途径，因此，不存在有完全不祈求于推论的发现过程。

“证明(proving)”是对于事先给定的结论和给定的前提（试图为该给定结论提供证据的已知事实或预设假说）寻找出从前提到结论的确切根据的过程。对于任何证明来说，如果没有事先给定的结论，那么绝对不能成为“证明”。

笔者提出基于强相关逻辑的推论来一般地解决ATF问题之研究方向的主要想法及其根据如下 [3-8]：

（1）自动推论/演绎研究领域以往工作及其应用的局限性，从本质上来说并非源于自动化方法本身，而是更深地源于自动化方法所基于的逻辑基础。

（2） “发现”在本质上不同于“证明”，所有的反证法（归谬法）对于“发现”来说都无济于事，唯有借助于向前推论方法（前推法）。

（3） 经典数理逻辑或者其经典保存扩张在原理上无法为推论提供逻辑正确性判断的逻辑基础。

（4） 相关逻辑（尤其是强相关逻辑）是在原理上能够为推论提供逻辑正确性判断逻辑基础的唯一逻辑系统族群。

（5） 从基于逻辑的形式理论的观点来看，在任何一个具体领域（不仅仅限于数学，也包括各种实际应用领域）里的自动定理发现问题可以归结到在该领域的基于相关逻辑的形式理论里自动发现经验定理的问题；一般的ATF问题可以归结为识别出在各种领域（不仅仅限于数学，也包括各种实际应用领域）的基于相关逻辑的形式理论群中发现经验定理之一般方法的特性。

（6） 从具体实际应用的角度来看，一个自动推论/演绎方法的健全性应该远比其完全性更重要，没有健全性作为前提保证的完全性不仅无益反而有害；如果一个自动推论/演绎方法在某个具体领域或者子领域具有健全性，那么即便是在该领域没有完全性，在具体实际应用中也可能会有相当大的实际意义。

（7） 开发一个独立于基础逻辑系统的自动推论/演绎系统是可能的；这样的自动推论/演绎系统对于各种具体实际应用是必要而方便的。

（8） 在任何一个具体领域（不仅仅限于数学，也包括各种实际应用领域）中，高度的概念和结论都是从最基本的概念和结论一步一步地抽象、组合成的，即便是很难、很高度的定理，其表述形式也不一定很复杂，有时甚至是相当简洁的。

关于基于逻辑的形式理论，请参看下图。图中红色部分 Th(L) 表示某个逻辑系统L的逻辑定理集合（可能是断片），蓝色部分 Th_L^e(P) 表示以某个具体领域的基础概念定义、经验公理以及已知或假设事实的集合 P 为前提，用 L 的推论规则和 Th(L) 中的逻辑定理推导出的所有结论（经验定理），那么，整个 Th(L)+Th_L^e(P) 便表达了以 L 为基础逻辑系统，P 为前提的一个形式理论。

众所周知，虽然经典命题逻辑（演算）是可判定的，但是经典一阶谓词逻辑（演算）是不可判定的，亦即，不存在一种能行可计算方法在有穷步骤内判定任意一个经典一阶谓词逻辑命题的真伪。然而，与经典数理逻辑相比，相关逻辑的命题逻辑部分就已经是不可判定的了 [18,19]。所以，作为经典数理逻辑的非经典保存扩张(non-classical conservative extension)，一般来说，有关相关逻辑的自动推论/演绎要比有关经典数理逻辑的自动推论/演绎要难很多。

笔者及其研究室沿着基于强相关逻辑的推论来一般地解决 ATF 问题的研究方向已经做了一些工作并且取得了一些初步结果 [3-8]。笔者做出的一个关键性选择（决定）是选取相关蕴含逻辑联结词在一个命题中的嵌套深度（被称为“degree(度，或者级)”）来作为分层次地定义、并且演绎地推导相关逻辑系统逻辑片段(fragment)的尺度标准，从而可以使得所有相关逻辑系统逻辑片段关于偏序包含关系形成一个半格。这一想法也应用到了针对某个具体领域的形式理论分层上去。我们开发了完全独立于基础逻辑系统的自动前推机 EnCal(处理一般二值逻辑系统)和FreeEnCal(处理包括有模态词的模态逻辑在内的各种逻辑系统)。我们以强相关谓词逻辑 EcQ 为基础逻辑系统，推导出其部分逻辑片段。我们以 EcQ 的逻辑片段为基础逻辑系统，分别以 NBG 公理集合论、初等数论(皮亚诺算术)、以及图论的基础概念定义和公理为前提，完全自动地推导出（再发现）了公理集合论、初等数论、以及图论的一些简单经验定理。这些初步结果显示，笔者所提倡的基于强相关逻辑的推论来一般地解决 ATF 问题这一研究方向还是很有希望的。

笔者根据 Wos 的 ATF 问题定义以及自己的研究实践认为，如何形式地定义清楚“新”和“有趣”，以及如何找到从大量结论中选择出让领域专家也能够认为是“新”和“有趣”的经验定理之判断标准，是一般地解决 ATF 问题的难中之难。另一方面，如果我们稍稍离开 Wos 的 ATF 问题定义，更多地从应用的角度来看，那么，要想得到某个具体领域的“新”和“有趣”的经验定理，更多地应用该领域的知识和经验，在适当的时候，请该领域的专家来参与判断，肯定是一条捷径。笔者在 1996 年提出的认识（认知）程序设计(epistemic programming)方法论，其基本思想就是为科学家和技术专家们提供表达领域知识和经验、定义择优标准、以及控制认知操作序列的手段，用自动前推机为科学家和技术专家们自动推导出经验定理并按照他们定义的择优标准选择出相对最优的经验定理供他们做出最终判定，并且提供对话方式的交互手段来对认识（认知）过程不断进行迭代 [20,21]。

从想要尽快得到某个具体领域的“新”和“有趣”的经验定理的应用角度来看，还有一个可行的途径是利用群体的力量，就像寻找巨大 Mersenne 素数的 GIMPS 计划一样。笔者在 2006 年提出的形式理论网格(theory grid)，就是这样一个计划 [22,23]。

尽管我们今天还没有完全地一般地解决 ATF 问题，但是我们为解决 ATF 问题所做的努力以及所得到的初步结果，已经开辟了崭新的应用方向，显示了广泛的应用前景。对于任何一个具体应用领域，如果我们已经掌握了一些知识而希图知道从这些知识出发我们能够得到什么新的事实或预测性结论，那么我们都可以把这归结为在该领域的自动定理发现，运用笔者提出的方法论和工具来解决。

综上所述，如果我们从形式理论的一般化角度来看，“自动定理发现”问题不仅仅对自动推论/演绎研究领域，并且对逻辑学、数学、哲学、认知科学、预测科学、计算机科学、人工智能等等诸多学科也应该是一个极具挑战性的基础研究问题。“自动定理发现”问题的一般性解决，不仅会给在本质上需要发现和预测功能的许多实际应用领域提供崭新的方法论和工具，而且还应该会为人类智能当中最本质最难通过计算来实现的运用知识进行推论并且从结论中择优的能力提供一个很好的“计算诠释”。

另一方面，宣传毫无科学根据的骇人听闻警告的那些“人工智能威胁人类论”者们，如果理解了“自动定理发现”问题解决之难度的话，是否会让自己的杞人忧天言行收敛一些呢？而如果他们连“自动定理发现”问题解决之难度都理解不了的话，我们还为什么要去理会那些所谓的警告呢？

参考文献

[1] L. Wos, “Automated Reasoning: 33 Basic Research Problems,” pp.  176-177, Prentice-Hall, 1988.

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

[3] 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.

[4] 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.

[5] J. Cheng, “EnCal: An Automated Forward Deduction System for General-Purpose Entailment Calculus,” in N. Terashima and E. Altman (Eds.), “Advanced IT Tools, IFIP World Conference on IT Tools, 2-6 September 1996, Canberra, Australia, IFIP ’96 - 14th World Computer Congress,” pp. 507-514, Chapman & Hall, September 1996.

[6] 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 Modelling and Knowledge Bases XI,” Frontiers in Artificial Intelligence and Applications, Vol. 61, pp. 136-159, IOS Press, February 2000.

[7] 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, Vietri sul Mare, Italy, September 12-14, 2007, Proceedings, Part II,” Lecture Notes in Artificial Intelligence, Vol. 4693, pp. 444-452, Springer, September 2007.

[8] 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.

[9] M. Davis, “The Early History of Automated Deduction,” in A. Robinson and A. Voronkov (Eds.), “Handbook of Automated Reasoning,” pp. 5-15, Elservier Science Publishers, 2001.

[10] M. Davis, “A Computer Program for Presbuger’s Algorithm,” in “Summaries of Talks Presented at the Summer Institute for Symbolic Logic,” Institute for Defense Analysis, 1957.

[11] A. Newell, J. Shaw, and H. Simon, “Empirical Explorations with the Logic Theory Machine,” in “Proceedings of West Joint Computer Conference,” pp. 218-239, 1957.

[12] H. Wang, “Toward Mechanical Mathematics,” IBM Journal of Research and Development, Vol. 4, pp. 2-22, 1960.

[13] H. Wang, “Proving Theorems by Pattern Recognition I,” Communications of the ACM, Vol. 3, pp. 220-234, 1960.

[14] H. Wang, “Popular Lectures on Mathematical Logic,” Science Press and Von Nostrand Reinhold, 1981; 王浩, “数理逻辑通俗讲话”，科学出版社, 1981; “Popular Lectures on Mathematical Logic (added a postscript),”Dover Publications, 1993.

[15] J.A. Robinson, “A Machine-oriented Logic Based on the Resolution Principle,” Journal of the ACM, Vol. 12, pp. 23-41, 1965.  

[16] 吴文俊, “初等几何的判定问题与定理机械化证明,” 中国科学, Vol. 20, No. 6, pp. 507-516, 1977.

[17] A. Quaife, “Automated Development of Fundamental Mathematical Theories,” Kluwer Academic Publishers, 1992.

[18]  A. R. Anderson and N. D. Belnap Jr., “Entailment: The Logic of Relevance and Necessity,” Vol. I, Princeton University Press, 1975.

[19]  A. R. Anderson, N. D. Belnap Jr., and J. M. Dunn, “Entailment: The Logic of Relevance and Necessity,” Vol. II, Princeton University Press, 1992.

[20] J. Cheng, “Epistemic Programming - Toward a New Programming Paradigm for Scientific Discovery,” Proceedings of the 37th Annaul Symposium on Programming, pp. 61-72, Hakone, Japan, IPSJ, January 1996.

[21] J. Cheng, “Epistemic Programming: Can We have a ‘Science’ and/or an ‘Engineering’ of Scientific Discovery in the 21st Century?” Proceedings of the 1999 IPSJ Annual Summer Symposium on Programming - The Dreams of the 21st Century, pp. 19-29, Fukushima, Japan, IPSJ, August 1999.

[22] J. Cheng, S. Nara, T. Koh, and Y. Goto, “The Theory Grid and Grid Theorists,” Proceedings of the 2nd International Conference on Semantics, Knowledge and Grid, IEEE Computer Society Press, November 2006.

[23] J. Cheng, Y. Goto, S. Nara, and T. Koh, “A Cooperative Grid Computing Approach to Automated Theorem Finding and Automated Problem Proposing,” in B. Apolloni, R. J. Howlett, and L. C. Jain (Eds.), “Knowledge-Based Intelligent Information and Engineering Systems, 11th International Conference, KES 2007, Vietri sul Mare, Italy, September 12-14, 2007, Proceedings, Part II,” Lecture Notes in Artificial Intelligence, Vol. 4693, pp. 840-851, Springer, September 2007.