The first-order predicate calculus is developed as a free variable theory using Skolem functions to define the quantifiers. The equivalence to ordinary first-order logic is proved.

The work of mathematical logician Emil Post is surveyed from the viewpoint of its relevance to computer science. Computational logic and production systems are first discussed. This is followed by an examination of Post's work on finite combinatory processes and reducibility.>

Since software testing cannot ordinarily be expected to provide conclusive evidence that a program is correct, software engineers have had to be satisfied with the vague notion of a set of test data being adequate for a given program. In this paper a theoretical model is provided for the notion of adequacy. Adequacy criteria are seen as serving to distinguish a given program from a certain class of programs. In particular, notions of distance between programs are studied, and adequacy of a test set is taken to mean that the set successfully distinguishes the program being tested from all programs that are sufficiently near to it, and differ in input-output behaviour from the given program. Certain points, called critical, are identified which must occur in every adequate test set. Finally, lower bounds are obtained on the size of test sets which are minimally adequate, in the sense that they have no adequate proper subsets.

Symbolic Logic and the American Mathematical Society, and supported financially by the Air Force Office of Scientific Research, the Institute for Defense Analyses, and the U. S. Army Research Office-Durham.The Symposium was presented in four sessions as follows: Session I -Computation with symbolic and algebraic data.Session II -Numerical methods for computers.Session I I I -Software systems; mechanical linguistics, computer analysis of language.Session IV -Theory of automata; artificial intelligence.An invited address was presented by Professor Hilary Putnam entitled, Constructible sets and predicative hierarchies.In addition nine papers were delivered, and six were presented by title; the last six abstracts below were those presented by title.

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 no decision procedure exists 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 by hand computation using 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

Hilbert's tenth problem is to find an algorithm for determining whether or not a diophantine equation possesses solutions. A diophantine predicate (of positive integers) is defined to be one of the form where P is a polynomial with integral coefficients (positive, negative, or zero). Previous work has considered the variables as ranging over nonnegative integers; but we shall find it more useful here to restrict the range to positive integers, no essential change being thereby introduced. It is clear that the recursive unsolvability of Hilbert's tenth problem would follow if one could show that some non-recursive predicate were diophantine. In particular, it would suffice to show that every recursively enumerable predicate is diophantine. Actually, it would suffice to prove far less.

It is an immediate consequence of results of Church and Gödel that there exist arithmetical recursively unsolvable problems, that is, recursively unsolvable problems of the form [M](P = Q) where P and Q are polynomials and [M] is some finite sequence of existential and universal quantifiers. A question which is immediately raised by this result is whether there exist unsolvable problems of this form where [M] is some finite sequence of existential quantifiers only. As a matter of fact this question is easily seen to be closely related to the tenth problem in the famous list proposed by Hilbert in 1900. In this paper, we prove the existence of recursively unsolvable problems of the form where P and Q are polynomials with non-negative integral coefficients. As a matter of fact we show that every recursively enumerable predicate is of the form (1), and conversely that every predicate of the form (1) is recursively enumerable. While our result does not yield the recursive unsolvability of Hilbert's tenth problem, it is easily seen that any considerable improvement of our result would yield this unsolvability. The author wishes to take this opportunity to express his gratitude to Professors Alonzo Church and E. L. Post with whom he has had the privilege of discussing some of the questions involved in this paper. He also wishes to thank his friends Melvin Hausner and Jacob Schwartz who have made valuable suggestions.