The problem of automated theorem finding
The problem of automated theorem finding
复制标题
自动定理发现问题
DOI：
10.1007/bf00881868
复制
发表时间：
1993
期刊：
影响因子：
--
通讯作者：
L. Wos
中科院分区：
文献类型：
--
作者：
L. Wos
本文是讨论自动推理中各种开放性研究问题的系列文章的第25篇。提出的研究问题要求一个人识别适当的属性，以允许自动推理程序找到新的和有趣的定理，而不是证明已证明的定理。这样的程序现在在许多领域作为有价值的推理助手发挥作用。如果他们也可以作为同事（可以这么说）自己进行研究，他们的价值就会急剧增加。
This article is the twenty-fifth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to identify appropriate properties to permit an automated reasoning program tofind new and interesting theorems, in contrast toproving conjectured theorems. Such programs are now functioning in many domains as valuable reasoning assistants. A sharp increase in their value would occur if they could also be used as colleagues to (so to speak) produce research on their own.