A Simplified Format for the Model Elimination Theorem-Proving Procedure

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A Simplified Format for the Model Elimination Theorem-Proving Procedure

Full text

Pdf (1.18 MB)

Source

Journal of the ACM (JACM) archive
Volume 16 , Issue 3 (July 1969) table of contents

Pages: 349 - 363

Year of Publication: 1969

ISSN:0004-5411

Author

D. W. Loveland

Carnegie-Mellon University, Pittsburgh, Pennsylvania

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 6, Downloads (12 Months): 39, Citation Count: 22

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/321526.321527 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	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]
	2	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]
	3	--. A review of utomtic theorem-proving. Proc. Syrup. Appl. Math., Amer. Math. Soc., Vol. 19, Provideace, R. L, 1966.

CITED BY 22

	L. J. Henschen, Theorem Proving by Covering Expressions, Journal of the ACM (JACM), v.26 n.3, p.385-400, july 1979
	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
	Robert Kowalski, Algorithm = logic + control, Communications of the ACM, v.22 n.7, p.424-436, July 1979
	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
	Jacques Cohen, A view of the origins and development of Prolog, Communications of the ACM, v.31 n.1, p.26-36, Jan. 1988
	Jürgen Dix , Ulrich Furbach , Ilkka Niemelä, Nonmonotonic reasoning: towards efficient calculi and implementations, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	Reinhold Letz , Gernot Stenz, Model elimination and connection tableau procedures, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	Richard A. Hagen , Scott Goodwin , Abdul Sattar, Code improvements for model elimination based reasoning systems, Proceedings of the 27th Australasian conference on Computer science, p.233-240, January 01, 2004, Dunedin, New Zealand
	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
	Jack Minker, Control structure of a pattern-directed search system, ACM SIGART Bulletin
	Fumiaki Okushi , Allen Van Gelder, Persistent and Quasi-Persistent Lemmas in Propositional Model Elimination, Annals of Mathematics and Artificial Intelligence, v.40 n.3-4, p.373-401, March 2004
	Allen Van Gelder, Another look at graph coloring via propositional satisfiability, Discrete Applied Mathematics, v.156 n.2, p.230-243, January, 2008
	Fumiaki Okushi, Parallel cooperative propositional theorem proving, Annals of Mathematics and Artificial Intelligence, v.26 n.1-4, p.59-85, 1999
	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 , Fumiaki Okushi, Lemma and cut strategies for propositional model elimination, Annals of Mathematics and Artificial Intelligence, v.26 n.1-4, p.113-132, 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
	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
	Shaul Markovitch , Paul D. Scott, Utilization filtering: a method for reducing the inherent harmfulness of deductively learned knowledge, Proceedings of the 11th international joint conference on Artificial intelligence, p.738-743, August 20-25, 1989, Detroit, Michigan
	James R. McSkimin , Jack Minker, The use of a semantic network in a deductive question-answering system, Proceedings of the 5th international joint conference on Artificial intelligence, p.50-58, August 22-25, 1977, Cambridge, 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
	Toni Bollinger, A model elimination calculus for generalized clauses, Proceedings of the 12th international joint conference on Artificial intelligence, p.126-131, August 24-30, 1991, Sydney, New South Wales, Australia