A COMPUTING PROCEDURE FOR QUANTIFICATION THEORY
A COMPUTING PROCEDURE FOR QUANTIFICATION THEORY
复制标题
DOI：
10.1145/321033.321034
复制
发表时间：
1960-01-01
影响因子：
2.5
通讯作者：
PUTNAM, H
中科院分区：
文献类型：
--
作者：
DAVIS, M;PUTNAM, H
在形式逻辑的研究中使用的数学方法将导致获得数学定理的纯计算方法的希望可以追溯到莱布尼茨，并在世纪之交被皮亚诺和希尔伯特学派在20世纪20年代复兴。希尔伯特注意到所有的经典数学都可以在量化理论中形式化，他宣称找到一种算法来确定给定的量化理论公式是否有效的问题是数学逻辑的中心问题。的确，对这一“决策”问题的调查一度似乎即将取得成功。然而，丘奇和图灵证明了这样的算法是不存在的。这一结果使人们对使用现代数字计算机来解决重大数学问题的可能性相当悲观。然而，最近人们对整个问题又重新产生了兴趣。具体地说，人们已经认识到，虽然量化理论不存在判定程序，但有许多证明程序是可用的——也就是说，统一的程序将最终为量化理论的任何公式找到有效的证明，但通常涉及在公式无效的情况下寻求“永远”——并且其中一些证明程序很可能被证明是可行的，可用于现代计算机器。王浩[9]和p.c. Gilmore[3]各自制作了使用量化理论证明程序的工作程序。Gilmore的程序采用了Herbrand的数学逻辑基本定理的一种形式，Wang的程序使用了根岑研究过的量化理论的一种表述。然而，这两个程序遇到决定性的困难，除了最简单的量化理论公式，在做命题演算的方法。Wang的程序，因为它使用了类似根岑的方法，涉及到对真功能连接词总数的求幂，而Gilmore的程序，使用标准形式，涉及到对现有子句数量的求幂。在许多情况下，这两种方法都优于真值表方法，后者涉及对存在的变量总数求幂，并代表重要的初始贡献，但在一些相当简单的例子中，这两种方法都遇到了困难。本文给出了量子化理论的一个统一证明过程，它适用于一些相当复杂的公式，通常不会导致幂次。Gilmore为IBM 704编写的程序使机器计算21分钟而没有得到结果，而用本方法在30分钟内成功地进行了手工计算，这一事实部分地表明了本程序比以前可用的程序的优越性。参见下文第6节。应该提到的是，在我们希望使用量化理论的证明程序来获得属于“真正的”数学的定理的证明之前，必须在数学的各个分支中获得有限公理化，这是“简短的”。最后一个问题在这里不再深入探讨；然而，参考Davis和Putnam的著作，他们给出了这个问题的一个解决方案
The hope that mathematical methods employed in the investigation of formal logic would lead to purely computational methods for obtaining mathematical theorems goes back to Leibniz and has been revived by Peano around the turn of the century and by Hilbert's school in the 1920's. Hilbert, noting that all of classical mathematics could be formalized within quantification theory, declared that the problem of finding an algorithm for determining whether or not a given formula of quantification theory is valid was the central problem of mathematical logic. And indeed, at one time it seemed as if investigations of this “decision” problem were on the verge of success. However, it was shown by Church and by Turing that such an algorithm can not exist. This result led to considerable pessimism regarding the possibility of using modern digital computers in deciding significant mathematical questions. However, recently there has been a revival of interest in the whole question. Specifically, it has been realized that while nodecision procedureexists for quantification theory there are many proof procedures available—that is, uniform procedures which will ultimately locate a proof for any formula of quantification theory which is valid but which will usually involve seeking “forever” in the case of a formula which is not valid—and that some of these proof procedures could well turn out to be feasible for use with modern computing machinery.Hao Wang [9] and P. C. Gilmore [3] have each produced working programs which employ proof procedures in quantification theory. Gilmore's program employs a form of a basic theorem of mathematical logic due to Herbrand, and Wang's makes use of a formulation of quantification theory related to those studied by Gentzen. However, both programs encounter decisive difficulties with any but the simplest formulas of quantification theory, in connection with methods of doing propositional calculus. Wang's program, because of its use of Gentzen-like methods, involves exponentiation on the total number of truth-functional connectives, whereas Gilmore's program, using normal forms, involves exponentiation on the number of clauses present. Both methods are superior in many cases to truth table methods which involve exponentiation on the total number of variables present, and represent important initial contributions, but both run into difficulty with some fairly simple examples.In the present paper, a uniform proof procedure for quantification theory is given which is feasible for use with some rather complicated formulas and which does not ordinarily lead to exponentiation. The superiority of the present procedure over those previously available is indicated in part by the fact that a formula on which Gilmore's routine for the IBM 704 causes the machine to computer for 21 minutes without obtaining a result was worked successfully byhand computationusing the present method in 30 minutes. Cf. §6, below.It should be mentioned that, before it can be hoped to employ proof procedures for quantification theory in obtaining proofs of theorems belonging to “genuine” mathematics, finite axiomatizations, which are “short,” must be obtained for various branches of mathematics. This last question will not be pursued further here; cf., however, Davis and Putnam [2], where one solution to this problem is given for ele