Theorem Proving by Covering Expressions

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Theorem Proving by Covering Expressions

Full text

Pdf (1.05 MB)

Source

Journal of the ACM (JACM) archive
Volume 26 , Issue 3 (July 1979) table of contents

Pages: 385 - 400

Year of Publication: 1979

ISSN:0004-5411

Author

L. J. Henschen

Department of Electrical Engineering and Computer Science, Northwestern University, Evanston, IL

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 20, Citation Count: 2

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/322139.322140 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	ANDREWS, P Refutations by mating, IEEE Trans. Comptrs (7-25 (1976), 801-806
	2	BOYER, R, AnD MOORE, J Shanng of structure m theorem proymg programs Machine Intelhgence 7, B. Meltzer and D Michle, Eds., Edinburgh U Press, Edinburgh, Scotland, 1972, pp 101-116
	3	Chin-Liang Chang , Richard C. Lee , Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, Inc., Orlando, FL, 1997
	4	GILMORE, P C A proof method for quantlficatton theory its justification and reahzatlon IBM J. Res and Develop 4 (1960), 28-35
	5	KOWALSKI, R, AND HAYES, P Semanuc trees m automatic theorem proving Machine Intelhgence 4, B Meltzer, and D. Mtchte, Eds, Edinburgh U Press, Edinburgh, Scotland, 1968, pp 87-101
	6	D. W. Loveland, A Simplified Format for the Model Elimination Theorem-Proving Procedure, Journal of the ACM (JACM), v.16 n.3, p.349-363, July 1969 [doi>10.1145/321526.321527]
	7	MIt~KEg, J, AND WILSON, G Resolution refinements A comparative study IEEE Trans Comptrs. (7-25 (1976), 782-800
	8	0VERBEEK, R., MCCHAREN, J, AND WOS, L Complextty and related enhancements for automated theorem proving programs Comp and Math wah Apphcatwns 2 (1976), i-16
	9	PRAWlTZ, D Advances and problems m mechamcal proof procedures Machine Intelhgence 4, B Meltzer and D Michte, Eds, Edinburgh U Press, Edinburgh, Scotland, 1968, pp 59-71
	10	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 [doi>10.1145/321250.321253]
	11	ROBINSON, G, AND WoS, L. Paramodulauon and theorem proving m first-order theories wRh equahty Machine lntelhgence 4, B Meltzer and D Mlchle, Eds, Edinburgh U Press, Edinburgh, Scotland, 1968, pp 135-150
	12	SHOSTAK, R. Refutation graphs. Aruf Intell 7 (1976), 51-64.
	13	SICKEL, S Clause mterconnectlvlty graphs m theorem proving IEEE Trans Comptrs. C-25 (1976), 823-834.
	14	YARMUSH, D The lmked conjunct and other algorithms for meehamcal theorem proving Rep. IMM-412, Courant Inst. Math Set, New York U, New York, July 1976

CITED BY 2

	Neil V. Murray , Erik Rosenthal, Inference with path resolution and semantic graphs, Journal of the ACM (JACM), v.34 n.2, p.225-254, April 1987
	Neil V. Murray , Erik Rosenthal, Path resolution with link deletion, Proceedings of the 9th international joint conference on Artificial intelligence, p.1187-1193, August 18-23, 1985, Los Angeles, California