Efficiency and Completeness of the Set of Support Strategy in Theorem Proving

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Efficiency and Completeness of the Set of Support Strategy in Theorem Proving

Full text

Pdf (378 KB)

Source

Journal of the ACM (JACM) archive
Volume 12 , Issue 4 (October 1965) table of contents

Pages: 536 - 541

Year of Publication: 1965

ISSN:0004-5411

Authors

Lawrence Wos	Argonne National Laboratory, Argonne, Illinois
George A. Robinson	Argonne National Laboratory, Argonne, Illinois
Daniel F. Carson	Argonne National Laboratory, Argonne, Illinois

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 38, Citation Count: 53

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/321296.321302 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	Wos, L., CARSON, D., AND ROBINSON, G. The unit preference strategy in theorem proving. AFIPS Conference Proceedings 26, Spartan Books, Washington, D. C., 1964, pp. 615-621.
	2	ROBINSON, G. A., Wos, L. T., AND CARSON, D .F . Some theorem-proving strategies and their implementation. AMD Tech. Memo. No. 72, Argonne Nat. Laboratory, 1964.
	3	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]

CITED BY 53

	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
	John K. Dixon, Z-Resolution: Theorem-Proving with Compiled Axioms, Journal of the ACM (JACM), v.20 n.1, p.127-147, Jan. 1973
	James R. Slagle, Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets, Journal of the ACM (JACM), v.19 n.1, p.120-135, Jan. 1972
	P. O'Hearn , Z. Stachniak, Note on theorem proving strategies for resolution counterparts of non-classical logics, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation, p.364-372, July 17-19, 1989, Portland, Oregon, United States
	Peter B. Andrews, Resolution With Merging, Journal of the ACM (JACM), v.15 n.3, p.367-381, July 1968
	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
	Bernard Elspas , Karl N. Levitt , Richard J. Waldinger , Abraham Waksman, An Assessment of Techniques for Proving Program Correctness, ACM Computing Surveys (CSUR), v.4 n.2, p.97-147, June 1972
	L. Henschen , Ross Overbeck , L. Wos, A theorem-proving language for experimentation, Communications of the ACM, v.17 n.6, p.308-314, June 1974
	Peter B. Andrews, A Correction Concerning Resolution, Journal of the ACM (JACM), v.15 n.4, p.720, Oct. 1968
	James R. Slagle, An Approach for Finding C-Linear Complete Inference Systems, Journal of the ACM (JACM), v.19 n.3, p.496-516, July 1972
	Lawrence Wos , George A. Robinson , Daniel F. Carson , Leon Shalla, The Concept of Demodulation in Theorem Proving, Journal of the ACM (JACM), v.14 n.4, p.698-709, Oct. 1967
	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
	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
	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
	Robert Kowalski, A Proof Procedure Using Connection Graphs, Journal of the ACM (JACM), v.22 n.4, p.572-595, Oct. 1975
	Donald W. Loveland, Mechanical Theorem-Proving by Model Elimination, Journal of the ACM (JACM), v.15 n.2, p.236-251, April 1968
	Gordon J. VanderBrug , Jack Minker, State-space problem-reduction, and theorem proving—some relationships, Communications of the ACM, v.18 n.2, p.107-119, Feb. 1975
	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
	R. Loganantharaj, DC parallelism of connection graph, Proceedings of the 1987 Fall Joint Computer Conference on Exploring technology: today and tomorrow, p.319-326, December 1987, Dallas, Texas, United States
	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
	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
	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
	Christoph Weidenbach, Combining superposition, sorts and splitting, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	J. A. Robinson, Logic and logic programming, Communications of the ACM, v.35 n.3, p.40-65, March 1992
	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
	L. Henschen , L. Wos, Unit Refutations and Horn Sets, Journal of the ACM (JACM), v.21 n.4, p.590-605, Oct. 1974
	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
	James R. Slagle, Interpolation Theorems for Resolution in Lower Predicate Calculus, Journal of the ACM (JACM), v.17 n.3, p.535-542, July 1970
	E. E. Sibert , D. Michie, Some Binary Derivation Systems, Journal of the ACM (JACM), v.21 n.2, p.175-190, April 1974
	Chee-Fen Yu , Benjamin W. Wah, Learning Dominance Relations in Combined Search Problems, IEEE Transactions on Software Engineering, v.14 n.8, p.1155-1175, August 1988
	J. Kljaich, Jr. , B. T. Smith , A. S. Wojcik, Formal Verification of Fault Tolerance Using Theorem-Proving Techniques, IEEE Transactions on Computers, v.38 n.3, p.366-376, March 1989
	Chih-Hung Wu , Shie-Jue Lee, KJ3: a tool assisting formal validation of knowledge-based systems, International Journal of Human-Computer Studies, v.56 n.5, p.495-524, April 2002
	D. Sarkar , S. C. De Sarkar, A Set of Inference Rules for Quantified Formula Handling and Array Handling in Verification of Programs Over Integers, IEEE Transactions on Software Engineering, v.15 n.11, p.1368-1381, November 1989
	D. Sarkar , S. C. De Sarkar, Some Inference Rules for Integer Arithmetic for Verification of Flowchart Programs on Integers, IEEE Transactions on Software Engineering, v.15 n.1, p.1-9, January 1989
	Jia Meng , Claire Quigley , Lawrence C. Paulson, Automation for interactive proof: first prototype, Information and Computation, v.204 n.10, p.1575-1596, October 2006
	Jun Ma , Wenjiang Li , Da Ruan , Yang Xu, Filter-based resolution principle for lattice-valued propositional logic LP(X), Information Sciences: an International Journal, v.177 n.4, p.1046-1062, February, 2007
	Branden Fitelson , Larry Wos, Missing Proofs Found, Journal of Automated Reasoning, v.27 n.2, p.201-225, August 2001
	William McCune , Larry Wos, Otter - The CADE-13 Competition Incarnations, Journal of Automated Reasoning, v.18 n.2, p.211-220, April 1997
	Steve Greenbaum, Violet, Journal of Automated Reasoning, v.18 n.2, p.259-264, April 1997
	O. L. Astrachan , D. W. Loveland, The Use of Lemmas in the Model Elimination Procedure, Journal of Automated Reasoning, v.19 n.1, p.117-141, August 1997
	David A. Plaisted , Yunshan Zhu, Ordered Semantic Hyper-Linking, Journal of Automated Reasoning, v.25 n.3, p.167-217, October 2000
	R. T. Chien , P. B. Maggs , F. A. Stahl, New directions in legal information processing, Proceedings of the November 16-18, 1971, fall joint computer conference, November 16-18, 1971, Las Vegas, Nevada
	Arjen Hommersom , Peter j. f. Lucas , Patrick Van bommel, Checking the quality of clinical guidelines using automated reasoning tools, Theory and Practice of Logic Programming, v.8 n.5-6, p.611-641, November 2008
	K. Biss , R. Chien , F. Stahl, R2: a natural language question-answering system, Proceedings of the May 18-20, 1971, spring joint computer conference, May 18-20, 1971, Atlantic City, New Jersey
	Guillaume Burel , Gilles Dowek, How can we prove that a proof search method is not an instance of another?, Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, August 02-02, 2009, Montreal, Quebec, Canada
	L. Wos, Automated reasoning: real uses and potential uses, Proceedings of the Eighth international joint conference on Artificial intelligence, p.867-876, August 08-12, 1983, Karlsruhe, West Germany
	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
	Ricardo Caferra , Nicolas Peltier, Extending semantic resolution via automated model building: applications, Proceedings of the 14th international joint conference on Artificial intelligence, p.328-334, August 20-25, 1995, Montreal, Quebec, Canada
	David Gelperin, Deletion-directed search in resolution-based proof procedures, Proceedings of the 3rd international joint conference on Artificial intelligence, p.47-50, August 20-23, 1973, Stanford, USA
	Cordell Green, Application of theorem proving to problem solving, Proceedings of the 1st international joint conference on Artificial intelligence, p.219-239, May 07-09, 1969, Washington, DC
	C. L. Chang, Resolution plans in theorem proving, Proceedings of the 6th international joint conference on Artificial intelligence, p.143-148, August 20-23, 1979, Tokyo, Japan
	J. R. Slagle , C. L. Chang , R. C. T. Lee, Completeness theorems for semantic resolution in consequence-finding, Proceedings of the 1st international joint conference on Artificial intelligence, p.281-285, May 07-09, 1969, Washington, DC
	James B. Morris, E-resolution: extension of resolution to include the equality relation, Proceedings of the 1st international joint conference on Artificial intelligence, p.287-294, May 07-09, 1969, Washington, DC