Completeness of Linear Refutation for Theories with Equality

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Completeness of Linear Refutation for Theories with Equality

Full text

Pdf (569 KB)

Source

Journal of the ACM (JACM) archive
Volume 18 , Issue 1 (January 1971) table of contents

Pages: 126 - 136

Year of Publication: 1971

ISSN:0004-5411

Authors

C. L. Chang	National Institutes of Health, Division of Computer Research and Technology, Public Health Service, Department of Health, Education and Welfare, Bethesda, Maryland
J. R. Slagle	National Institutes of Health, Division of Computer Research and Technology, Public Health Service, Department of Health, Education and Welfare, Bethesda, Maryland

Publisher

ACM New York, NY, USA

Bibliometrics

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

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/321623.321636 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	CHANG, C.L. Renamable paramodulation for automatic theorem proving with equality. Heuristics Laboratory, Division of Computer Research and Technology, National Institutes of Health, Bethesda, Maryland, 1968; Artificial Intelligencv J. (to appear).
	3	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]
	4	DARLINGTON, J .L . Automatic theorem proving with equality substitutions and mathematical induction. In Machine Intelligence S, E. Dale and D. Michie, Eds., Oliver & Boyd, Edinburg, 1968, pp. 77-93.
	5	ERNST, G., AND NEWELL, A. GPS: A Casv Study in Generality and Problem Solving. Academic Press, New York, 1969.
	6	LOVELAND, D.W. A linear format for resolution. Proc. IRIA Symposium on Automatic Demonstration, 1968, Versailles, France. Springer-Verlag, 1970, pp. 147-162.
	7	LUCKHAM, D. Refinement Theories in Resolution Theory. Ibid., pp. 163-190.
	8	MORRIS, J. B. E-resolution: Extension of resolution to include the equality relation. Proc. International Joint Conference on Artificial Intelligence, 1969, pp. 287-294.
	9	ROBINSON, G., AND WOS, L. Paramodulation and theorem-proving in first-order theories with equality. In Machine Intelligence $, E. Dale and D. Michie, Eds., Oliver & Boyd, Edinburg, 1969, pp. 135-150.
	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, J .A . The generalized resolution principle. In Machine Intelligence S, E. Dale and D. Michie, Eds., Oliver & Boyd, Edinburg, 1968, pp. 77-93.
	12	SIBERT, E .E . A machine-oriented logic incorporating the equality relation. In Machine Intellig6nce $, E. Dale and D. Michie, Eds., Oliver & Boyd, Edinburg, 1969, pp. 103-133.
	13	James R. Slagle , Philip Bursky, Experiments With a Multipurpose, Theorem-Proving Heuristic Program, Journal of the ACM (JACM), v.15 n.1, p.85-99, Jan. 1968 [doi>10.1145/321439.321444]
	14	SLAGLE, J. R., AND KONIVER, D. Finding resolution proofs and using duplicate goals in AND/OR trees. Inform. Sci. J. (to appear).
	15	Wos, L., AND ROBXNSON, G. Paramodulation and set of support. Proc. IRIA Symposium on Automatic Demonstration, Versailles, France, 1968, Springer-Verlag, 1970, pp. 276- 310.

CITED BY 3

	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
	L. Henschen , L. Wos, Unit Refutations and Horn Sets, Journal of the ACM (JACM), v.21 n.4, p.590-605, Oct. 1974
	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