Semi-Automated Mathematics

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Semi-Automated Mathematics

Full text

Pdf (999 KB)

Source

Journal of the ACM (JACM) archive
Volume 16 , Issue 1 (January 1969) table of contents

Pages: 49 - 62

Year of Publication: 1969

ISSN:0004-5411

Authors

J. R. Guard	Applied Logic Corporation, Princeton, New Jersey
F. C. Oglesby	Applied Logic Corporation, Princeton, New Jersey
J. H. Bennett	Applied Logic Corporation, Princeton, New Jersey
L. G. Settle	Applied Logic Corporation, Princeton, New Jersey

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 22, Citation Count: 4

Additional Information:

abstract references cited by index terms collaborative colleagues peer to peer

Tools and Actions:	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/321495.321500 What is a DOI?

ABSTRACT

The fifth in a series of experiments in semi-automated mathematics is described. These experiments culminated in large complex computer programs which allow a mathematician to prove mathematical theorems on an man/machine basis. SAM V, the fifth program, is oriented primarily toward the development of efficient automatic techniques for handling some of the more basic processes of mathematical deduction, and toward the realization of efficient real-time interaction between man and machine through the use of cathode-ray tube displays. SAM V's most notable success is the solution of an open problem in lattice theory.

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	BENNETT, J. H., EASTON, W. B., GUARD, J. R., AND MOTT, JR., T .H . Introduction to semi-automated mathematics. Final Rep. No. AFCRL 63-180, Air Force Cambridge Res. Lab., Cambridge, Mass., April 15, 1963 (Contract No. AF 19(628)-468).
	2	GUARD, J.R. Automated logic for semi-automated mathematics. Sei. Rep. No. 1, AFCI 64-411, March 30, 1964 (Contract No. AF 19(628)-3250).
	3	BENNETT, J. H., EASTON, W. B., GUARD, Y. R., AND MOTT, JR., T. H. Toward semi. automated mathematics: the language and logic of SAM III. Sci. Rep. No. 2, AFCIiL 64-562, May 1, 1964 (Contract No. AF 19(628)-3250).
	4	BENNETT, J. H., EASTON, W. B., GUARD, J. R., LOVEMAN, D. B., AND MOTT, JR., T. Semi-automated mathematics: SAM IV. Sci. Rep. No. 3, AFCRL 64-827, Oct. 15, 1961 (Contract No. AF 19 (628)-3250).
	5	BENNETT, J. H., EASTON, W. B., GUARD, J. R., .AND SETTLE, L. G. CRT-aided semiautomated mathematics. Final Rep. No. AFCRL 67-017, Jan. 1967 (Contract No. AF 19(628)-3250).
	6	GOULD, W.E. A matching procedure for -order logic. Sci. Rep. No. 4, AFCRL 66-781, Oct. 15, 1966 (Contract No. AF 19(628)-3250).
	7	BUMCEOT, ROBERT. Proc. Glasgow Math. Assoc. 7, Pt. 1 (1965), pp. 22--23.

CITED BY 4

	James R. Slagle, Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity, Journal of the ACM (JACM), v.21 n.4, p.622-642, Oct. 1974
	Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980
	Joseph L. Bates , Robert L. Constable, Proofs as programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.1, p.113-136, Jan. 1985
	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