A Unifying View of Some Linear Herbrand Procedures

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A Unifying View of Some Linear Herbrand Procedures

Full text

Pdf (1.07 MB)

Source

Journal of the ACM (JACM) archive
Volume 19 , Issue 2 (April 1972) table of contents

Pages: 366 - 384

Year of Publication: 1972

ISSN:0004-5411

Author

D. W. Loveland

Mathematics Department and Computer Science Department, Carnegie-Mellon University, Pittsburgh, PA

Publisher

ACM New York, NY, USA

Bibliometrics

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

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/321694.321706 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	C. L. Chang, The Unit Proof and the Input Proof in Theorem Proving, Journal of the ACM (JACM), v.17 n.4, p.698-707, Oct. 1970 [doi>10.1145/321607.321618]
	3	DAVIS, M. Eliminating the irrelevant from mechanical proofs. In Proceedings of Symposia in Applied Mathematics XV American Mathematical Society, Providence, R. I., 1963, pp. 15-30.
	4	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]
	5	HAYES, P., AND KOWALSKI, R. Sematic trees in automatic theorem-proving. Machine Intelligence 4 (B. Meltzer and D. Michie, Eds.), Edinburgh U. Press, Edinburgh, 1969, pp. 87-102.
	6	KOWALSKI, }~., AND KUEHNER, D. Linear resolution with selection function. Memo 34, Metamathematics Unit, Edinburgh U., Scotland (Oct. 1970).
	7	Donald W. Loveland, Mechanical Theorem-Proving by Model Elimination, Journal of the ACM (JACM), v.15 n.2, p.236-251, April 1968 [doi>10.1145/321450.321456]
	8	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]
	9	LOVELAND, D. W. Theorem provers combining model elimination and resolution. Machine Intelligence 4 (B. Meltzer and D. Michie, Eds.), Edinburgh U. Press, Edinburgh, 1969, pp. 73-86.
	10	LOVELAND, D.W. A linear format for resolution. Lecture Notes in Mathematics 125 (Symposium on Automatic Demonstratiou), Springer-Verlag, Berlin, 1970, pp. 147-162.
	11	LOVELAND, 1). W. A brief primer oil resolution proof procedures. Computer Science Research Review, 1970-1971, Carnegie-Mellon U., Sept. 1971, pp. 7-19.
	12	LOVELAND, D. W. Some linear Herbrand proof procedures: An analysis. Comput. Sci. Rep., Carnegie-Mellon U. (Dec. 1970).
	13	LUCKHAM, D. Refinement theorems in resolution theory. Lecture Notes in Mathematics 125 (Symposium oft. Automatic Demonstratio~l), Springer-Verlag, Berlin, 1970, pp. 163-190.
	14	Allen Newell , H. A. Simon, GPS, a program that simulates human thought, Computers & thought, MIT Press, Cambridge, MA, 1995
	15	PRAWITZ, D. Advances and problems in mechanical proof procedures. Machine Intelligence 4 (B. Meltzer and D. Michie, Eds.), Edinburgh U. Press, Edinburgh, 1969, pp. 59- 71.
	16	PRAWITZ, 1). A proof procedure with matrix reduction. Lecture Notes in Mathematics 125 (Symposium on Automatic Demonstration). Springer-Verlag, Berlin, 1970, pp. 207-214.
	17	Raymond Reiter, Two Results on Ordering for Resolution with Merging and Linear Format, Journal of the ACM (JACM), v.18 n.4, p.630-646, Oct. 1971 [doi>10.1145/321662.321678]
	18	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]
	19	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]
	20	Wos, L., CARSON, D., AND ROBINSON, G. The unit preference strategy in theorem proving. Proc. AFIPS 1964 FJCC, Vol. 26, Pt. 1, Spartan Books, New York, pp. 615-621.
	21	YATES, R., RAPH.~_EL, B., AND HART, T. Resolution graphs. Artificial Intelligence Group Tech. Note 24, Stanford Research Institute (1970).

CITED BY 10

	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
	Amaryllis Deliyanni , Robert A. Kowalski, Logic and semantic networks, Communications of the ACM, v.22 n.3, p.184-192, March 1979
	Reinhold Letz , Gernot Stenz, Model elimination and connection tableau procedures, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	John F. Sowa, Semantics of conceptual graphs, Proceedings of the 17th annual meeting on Association for Computational Linguistics, June 29-July 01, 1979, La Jolla, California
	S. Fleisig , D. Loveland , A. K. Smiley, III , D. L. Yarmush, An Implementation of the Model Elimination Proof Procedure, Journal of the ACM (JACM), v.21 n.1, p.124-139, Jan. 1974
	Allen Van Gelder , Fumiaki Okushi, A propositional theorem prover to solve planning and other problems, Annals of Mathematics and Artificial Intelligence, v.26 n.1-4, p.87-112, 1999
	Allen Van Gelder, Autarky Pruning in Propositional Model Elimination Reduces Failure Redundancy, Journal of Automated Reasoning, v.23 n.2, p.137-193, August 1999
	David Sturgill , Alberto Maria Segre, Nagging: A Distributed, Adversarial Search-Pruning Technique Applied to First-Order Inference, Journal of Automated Reasoning, v.19 n.3, p.347-376, December 1997
	Harry E. Pople, On the mechanization of abductive logic, Proceedings of the 3rd international joint conference on Artificial intelligence, p.147-152, August 20-23, 1973, Stanford, USA
	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