“基于强相关逻辑演算的自动定理发现”之原始创新论文

程京德

这是本人 1994 年和 1995 年的两篇论文，开创了“基于强相关逻辑演算的自动定理发现”这一新研究方向，是笔者研究室在这一研究方向上所有工作的初始基础。现将两篇论文存放于此，一方面留作保存记录，另一方面提供给听课学生和有兴趣者获取。

下面的图片，是司马贺(Herbert A. Simon, 1916-2001, “人工智能”和“认知科学”创始者之一，1975年图灵奖、1978年诺贝尔经济学奖获奖者)在 AAAI 1995 Spring Symposium (斯坦福大学) 上与笔者讨论此研究方向时留给笔者的签名，也一并存放于此，留作纪念。

顺便把论文概要翻译为中文如下：

FGCS94 Workshop 论文： “由 Wos 提出的自动定理发现问题寻求一种标准能够让自动推理程序用于发现新的和有趣的定理，而不是证明那些由用户提供的猜想的定理。本文从相关逻辑的角度讨论了自动定理发现的逻辑基础。本文指出为什么古典数学逻辑或其各种扩张不是解决该问题的合适的逻辑工具，并且说明无悖论的相关逻辑是更有希望的候选。本文还介绍了使用 EnCal，我们正在开发的一个通用自动前推机，所进行的 NBG 集合论自动定理发现的一些实验结果。”

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.

Abstract：“The problem of automated theorem finding proposed by Wos asks for criteria that an automated reasoning program can use to find new and interesting theorems, in contrast to proving conjectured theorems supplied by the user. This paper discusses the logical basis of automated theorem finding from the viewpoint of relevant logic.  The paper points out why classical mathematical logic and/or its various extensions are not suitable logical tools for solving the problem, and shows that paradox-free relevant logics are more hopeful candidates for the purpose.  The paper also presents some results of our experiments on automated theorem finding in NBG set theory with EnCal, an entailment calculus system we are developing.”

PDF: ATF_FGCS94W.pdf

司马贺(Herbert A. Simon)签名

AAAI SS95 论文： “任何科学发现必须包括一个认识过程，以获得关于某些经验的或逻辑的归结蕴涵之知识或者确定以前未知或未被认识的某些经验的或逻辑的归结蕴涵的存在。在此认识过程中的演绎认识操作是从作为前提的已知事实或假定中逻辑地发现新的有效的归结蕴涵。自动定理发现可以被认为是这种演绎认识操作的自动化。本文从相关逻辑的角度讨论了自动定理发现的逻辑基础。本文指出为什么古典数学逻辑或其各种扩张不是解决该问题的合适的逻辑工具，并且说明无悖论的相关逻辑是更有希望的候选。”

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

Abstract：“Any scientific discovery must includean epistemic process to gain knowledge of or to ascertain the existence of some empirical and/or logical entailments previously unknown or unrecognized.  The epistemic operation of deduction in an epistemic process of an agent is to find new and valid entailments logically from some premises which are known facts and/or assumed hypothesis.  Automated theorem finding can be regarded as the automation of deduction operations of an agent.  This paper discusses the logical basis of automated theorem finding from the viewpoint of relevant logic.  The paper points out why classical mathematical logic and/or its various extensions are not suitable logical tools for solving the problem, and shows that paradox-free relevant logics are more hopeful candidates for the purpose.”

PDF: ATF_AAAI-SS-95-03.pdf