1

W. ACKERMANN. Solvable Cases of the Decision Problem. 114 pp., 1954, Amsterdam.

2

ALONZO CHURCH Special cases of the decision problem, Revue philosophique de Louvain 49 (1951), 203-221 ; a corvection, ibid., 50 (1952), 279-272.

3

ALONZO CHURCH. Introduclion lo Mathentatical Logie, I 376 pp., 1956, Princeton.

4

M. DAVIS AND H. PUTNAM. A computational proof procedure. AFOSR, 1959 (submitted to Journal of Association for Computing Machinery).

5

B. DREBEN. On the completeness of quantification theory. Proc. Nat. Acad. Sci, USA, 38 (1952), 1047-1052.

6

B. DREBEN. Systematic treatinent of the decision problem. Summaries of talks at the Summer Institute of Symbolic Logic, p. 36:1, 11957, Cornell.

7

B. DUNHAM, R. FRIDSHAL, AND G. L. SWARD. A nonheuriaie program for proving clement ary logical theorems (abstrct). Comm. ACM , 2 (1959), 19 20.

8

P. C. GILMORE. A proof method for quantification theory its justificalion and realization. IBM J, Res. Develop. (1960), 28-35.

9

J. HERBRAND. Recherches sur la Theorie de la Demontication. 128 pp., 1930, Warsaw.

10

J. HERBRAND. Sur le prohleme fundamental de la logique mathematique Compt, rend. Soc. Sci. Lettres Varsorie, Classe III, 24 (1931), 12-56.

11

K. J. J. HINTIKKA. Vicious circle principle and the paradox J. Symbol. Logic, 22 (1957), 2,15-249.

12

L. KALMAR. Uber die Erfullbarkeit derjenigen Zahlausdrucke, welehe in der Normalform zwei benachbarte Allzeichen enthalten. Math.. Ann. 108 (1933), 466-484.

13

DIETER KLACA. Systematische Behandling der losbaren Falle des Entseheidungsprobtcms fur den Pradikatenkalkul der ersten Stufe. Zeil. math. Logik Grundl. Math. 1 (1955 264-270.

14

E. LANDAU. Grundlagen der Analysis, 1930, Leizig.

15

W. V. QUINE. Methods of Logic. 1950 and 1958, New York

16

T. SKOLEM. Uber die mathmatische Logik. Norsk Mat. Tidsskrift, 10 (1928), 125-142.

17

E. SPECKER. The axiom of choice in Quinc's new foundations for mathematical logic. Proc. Nat. Acad. Sci. USA, 28 (1953), 972-975.

18

HAO WANG. A theory of constructive types. Methods 1 (1949) 374-384.

19

HAO WANG. Circuit synthesis by solving sequential Boolean equations. Zeit. math. Logik Grundl. Mathe. 5 (1959), 29b.322.

20

HAO WANG. Toward mechanical mathematics. IBM J., Res. Develop. 4 (1960), 2-22.

Joyce Friedman, A Computer Program for a Solvable Case of the Decision Problem, Journal of the ACM (JACM), v.10 n.3, p.348-356, July 1963

Saul Gorn, Mechanical languages: a course specification, Communications of the ACM, v.7 n.4, p.219-222, April 1964

Gordon Beavers , Hal Berghel, “Dynamic” inferencing with generalized resolution, Proceedings of the 1993 ACM/SIGAPP symposium on Applied computing: states of the art and practice, p.614-621, February 14-16, 1993, Indianapolis, Indiana, United States

S. C. van Westrhenen, Statistical Studies of Theoremhood in Classical Propositional and First Order Predicate Calculus, Journal of the ACM (JACM), v.19 n.2, p.347-365, April 1972

Joyce Friedman, A Semi-Decision Procedure for the Functional Calculus, Journal of the ACM (JACM), v.10 n.1, p.1-24, Jan. 1963

William F. Atchison , Samuel D. Conte , John W. Hamblen , Thomas E. Hull , Thomas A. Keenan , William B. Kehl , Edward J. McCluskey , Silvio O. Navarro , Werner C. Rheinboldt , Earl J. Schweppe , William Viavant , David M. Young, Jr., Curriculum 68: Recommendations for academic programs in computer science: a report of the ACM curriculum committee on computer science, Communications of the ACM, v.11 n.3, p.151-197, March 1968

William S. Cooper, Fact Retrieval and Deductive Question-Answering Information Retrieval Systems, Journal of the ACM (JACM), v.11 n.2, p.117-137, April 1964

J. A. Robinson, Theorem-Proving on the Computer, Journal of the ACM (JACM), v.10 n.2, p.163-174, April 1963

Donald MacKenzie, The Automation of Proof: A Historical and Sociological Exploration, IEEE Annals of the History of Computing, v.17 n.3, p.7-29, September 1995