THEOREM-PROVING ON COMPUTER
THEOREM-PROVING ON COMPUTER
复制标题
DOI：
10.1145/321160.321166
复制
发表时间：
1963-01-01
影响因子：
2.5
通讯作者：
ROBINSON, JA
中科院分区：
文献类型：
--
作者：
ROBINSON, JA
在量化理论的文献中，对于从一组给定前提得出的给定结论，要找到证明（如果存在）的问题的表述有很好的解释。特别是，[1]和[3]中展示了如何将原始问题转换为不包含量词且由析取的合取组成的标准形式，每个析取是一个开放原子句子形式或一个的否定。我们假设熟悉这些表述和初步转换的方法，并仅提供本文直接目的所需的工作术语的定义。本文讨论了体现证明构造过程的计算机程序遇到的“组合爆炸”困难。描述了阿贡国家实验室开发的一个项目，其中通过两种方式在一定程度上缓解了这些困难。第一种方法虽然在实践中非常有用，但在智力上不如第二种方法令人满意，它本质上是将程序的数学家用户合并到 searchqoop 中。通过这种方式获得的证明的几个例子被展示和讨论，它们的一个有趣的特征是它们是“相当重要的”数学练习。第二种方法涉及完整的证明程序，这对于文献来说似乎是新的，但尚未被编程和测试。
There are excellent explanations in the literature of the formulation, in quantification theory, of problems in which a proof is to be found, ff one exists, for a given conclusion from a set of given premises. In particular, in [1] and [3] it is shown how to transform the original problem into a standard form which contains no quantifiers and which consists of a conjunction of disjunctions, each disjunct being an open atomic sentence-form or the negation of one. We assume familiarity with these methods of formulation and preliminary transformation, and provide just those definitions of our working terminology which will be required for the immediate purposes of the paper. The paper discusses the" combinatorial explosion" difficulties encountered by computer programs embodying proof-construction procedures. A program developed at Argonne National Laboratory is described in which these difficulties are somewhat alleviated in two ways. The first way, which although very useful in practice is less intellectually satisfying than the second way, consists essentially in incorporating the mathematician-user of the program into the searchqoop. Several examples of proofs obtained by this means are exhibited and discussed, one interesting feature of them being that they are" reasonably nontrivial" mathematical exercises. The second way involves a complete proof procedure which seems to be new to the literature but which has not yet been programmed and tested.