Two Results on Ordering for Resolution with Merging and Linear Format

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Two Results on Ordering for Resolution with Merging and Linear Format

Full text

Pdf (754 KB)

Source

Journal of the ACM (JACM) archive
Volume 18 , Issue 4 (October 1971) table of contents

Pages: 630 - 646

Year of Publication: 1971

ISSN:0004-5411

Author

Raymond Reiter

University of British Columbia, Department of Computer Science, Vancouver, British Columbia, Canada

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 0, Downloads (12 Months): 19, Citation Count: 11

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/321662.321678 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	Robert Anderson , W. W. Bledsoe, A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness, Journal of the ACM (JACM), v.17 n.3, p.525-534, July 1970 [doi>10.1145/321592.321603]
	2	Peter B. Andrews, Resolution With Merging, Journal of the ACM (JACM), v.15 n.3, p.367-381, July 1968 [doi>10.1145/321466.321469]
	3	DARLINGTON, J. L. Theorem proving and information retrieval. Machine Intelligence, Vol. 4. B. Meltzer and D. Michie, Eds. American Elsevier, New York, 1969.
	4	KOWALSKI, R., AND HAYES, P. Semantic trees in automatic theorem-proving. Machine Intelligence, Vol. ~4. B. Meltzer and D. Michie, Eds. American Elsevier New York, 1969.
	5	LOVELAND, D. A linear format for resolution. Symposium on Automatic Demonstration. M. Laudet, Ed. Springer-Verlag, New York, 1970.
	6	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]
	7	James R. Slagle, Automatic Theorem Proving With Renamable and Semantic Resolution, Journal of the ACM (JACM), v.14 n.4, p.687-697, Oct. 1967 [doi>10.1145/321420.321428]
	8	Lawrence Wos , George A. Robinson , Daniel F. Carson, Efficiency and Completeness of the Set of Support Strategy in Theorem Proving, Journal of the ACM (JACM), v.12 n.4, p.536-541, Oct. 1965 [doi>10.1145/321296.321302]
	9	YATES, R., RAPHAEL, B., AND HART, T. Resolution graphs. SRI Artificial Intelligence Memo, Stanford Research Institute, Menlo Park, California (Jan. 1970).

CITED BY 11

	M. H. Van Emden , R. A. Kowalski, The Semantics of Predicate Logic as a Programming Language, Journal of the ACM (JACM), v.23 n.4, p.733-742, Oct. 1976
	D. W. Loveland, A Unifying View of Some Linear Herbrand Procedures, Journal of the ACM (JACM), v.19 n.2, p.366-384, April 1972
	James R. Slagle , Lewis M. Norton, Experiment with an automatic theorem-prover having partial ordering inference rules, Communications of the ACM, v.16 n.11, p.682-688, Nov. 1973
	Robert A. Kowalski, The early years of logic programming, Communications of the ACM, v.31 n.1, p.38-43, Jan. 1988
	Jieh Hsiang , Michaël Rusinowitch, Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method, Journal of the ACM (JACM), v.38 n.3, p.558-586, July 1991
	Herve Gallaire , Jack Minker , Jean-Marie Nicolas, Logic and Databases: A Deductive Approach, ACM Computing Surveys (CSUR), v.16 n.2, p.153-185, June 1984
	Jack Minker, In memoriam: Raymond Reiter, AI Magazine, v.24 n.1, p.13-18, March 2003
	Jack Minker, In Memoriam: RAYMOND REITER June 12, 1939 – September 16, 2002, Theory and Practice of Logic Programming, v.3 n.1, p..1-.9, January 2003
	G. A. Ringwood, SLD: a folk acronym?, ACM SIGPLAN Notices, v.24 n.5, p.71-75, May 1989
	D. W. Loveland , M. E. Stickel, A hole in goal trees: some guidance from resolution theory, Proceedings of the 3rd international joint conference on Artificial intelligence, p.153-161, August 20-23, 1973, Stanford, USA
	Katsumi Inoue, Consequence-finding based on ordered linear resolution, Proceedings of the 12th international joint conference on Artificial intelligence, p.158-164, August 24-30, 1991, Sydney, New South Wales, Australia