Theorem-Proving on the Computer

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Theorem-Proving on the Computer

Full text

Pdf (704 KB)

Source

Journal of the ACM (JACM) archive
Volume 10 , Issue 2 (April 1963) table of contents

Pages: 163 - 174

Year of Publication: 1963

ISSN:0004-5411

Author

J. A. Robinson

Department of Philosophy, Argonne National Laboratory and Rice University

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 9, Downloads (12 Months): 45, Citation Count: 8

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/321160.321166 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
	2	Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
	3	DAvis, MarTIN. Eliminating the irrelevant from mechanical proofs. Paper, Syrup. Exp. Arith., A.M.S. Meeting no. 589, Apr. 1962 (Mimeo.).
	4	PRawITz, DaG. An improved proof procedure. Theories 26 (1960), 102-1:39.
	5	WaNG, Hao. Towards mechanical mathematics. IBM J. IRes. Develop. 4 (1960), 2-22.
	6	Hao Wang, Proving theorems by pattern recognition I, Communications of the ACM, v.3 n.4, p.220-234, April 1960 [doi>10.1145/367177.367224]
	7	WANG, Hao. Proving theorems by pattern recognition, II. Bell Sgsten Tech. Y. 40 "(1961), 1-41.
	8	GILOR:, P.rL C. A proof method for quantification theory. IBM J. Res. Develop. 4 (1960), 28-35.
	9	Dag Prawitz , Haå kan Prawitz , Neri Voghera, A Mechanical Proof Procedure and its Realization in an Electronic Computer, Journal of the ACM (JACM), v.7 n.2, p.102-128, April 1960 [doi>10.1145/321021.321023]
	10	tZOBNSON, J .A . A general theorem-proving program for the IBM 704. Argonne Nat. Lab. Rep. 6447, Nov. 1961.
	11	QtTtNE, W.V. Methods of Logic. Henry Holt, New York, rev. ed. (1959).
	12	QuINE, W. V. A proof procedure for quantification theory. J. Symbolic Logic P0 (1955), 141-149.
	13	BIRKHOFF, GaRRrT aND MACLtNE, SAUNDiqS. A Survey of Moder AlgeSra. Macmilan, rev. ed. (1953).
	14	BInXItOFF, GAnnETT. Lattice Theory. AMS Colloq. Pubt., Vol. 25, rev. ed. (1948).
	15	BETS, Every. Formf Methods. D. Reidel, Holland (1962).
	16	bose r C. and SHERIHANDS, S.S O N THE FALSITY OF EULERS conjectruer about the nonesistence of two orthonal latin squares of order 4t+ 2proc. nat.acad,sci 45 (1949), 734-737
	17	Parker, E. T. oirthogonal latin squares proc. nat. acds, sci., 45 1959, 859-862

CITED BY 8

	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
	Arthur J. Nevins, A Human Oriented Logic for Automatic Theorem-Proving, Journal of the ACM (JACM), v.21 n.4, p.606-621, Oct. 1974
	J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965
	Ross A. Overbeek, A New Class of Automated Theorem-Proving Algorithms, Journal of the ACM (JACM), v.21 n.2, p.191-200, April 1974
	Nachum Dershowitz , David A. Plaisted, Conditional rewriting, ACM SIGSOFT Software Engineering Notes, v.10 n.4, August 1985
	J. A. Robinson, Logic and logic programming, Communications of the ACM, v.35 n.3, p.40-65, March 1992
	Nicholas V. Findler, Human decision making under uncertainty and risk: computer-based experiments and a heuristic simulation program, Proceedings of the November 30--December 1, 1965, fall joint computer conference, part I, November 30-December 01, 1965, Las Vegas, Nevada
	Larry E. Travis, Experiments with a theorem-utilizing program, Proceedings of the April 21-23, 1964, spring joint computer conference, April 21-23, 1964, Washington, D.C.